How to prove that every clause that is implied by the input formula (learned or not) can be derived using resolution with weakening rule:
$\frac{C} {C \vee D}$
(A clause $C$ is implied by $F$ if for all possible assignments $A$ it holds that $F[A]\implies C[A]$.)
What proof of the completeness of resolution do you know? Chances are it can be easily adapted to this more general setting.
Alternatively, you can reduce it to plain completeness. One way is as follows. Assume a clause $C=l_1\lor\dots\lor l_k$ is implied by a CNF $F$. Then the CNF $F\land\let\ob\overline\ob{l_1}\land\dots\land\ob{l_k}$ is unsatisfiable, hence it has a resolution refutation. The only way one of the new axioms $\ob{l_i}$ can be used in the refutation is in a resolution step $$\dfrac{D\lor l_i\qquad\ob{l_i}}D.$$ So if you just omit these steps along with the $\ob{l_i}$ axioms, and perform the remaining inferences as before, you will end up with a valid resolution derivation from $F$ that differs from the original one only in that some extra literals from $C$ are included in some of the clauses. In particular, the derivation ends with a subclause of $C$, from which you can infer $C$ by weakening.
