[proofplan] Choose one injective resolution for each object of $\mathcal A$ and define $R^iF(A)$ as the $i$-th cohomology object of the complex obtained by applying $F$. A morphism $A \to A'$ is lifted to a cochain map between the chosen injective resolutions by induction, using injectivity at each stage. Any two such lifts are cochain homotopic, so they induce the same morphism on cohomology; this gives well-defined functorial maps. Finally, left exactness identifies the zeroth cohomology of $F(I_A^\bullet)$ with $F(A)$ naturally in $A$. [/proofplan] [step:Choose injective resolutions and define the candidate objects] For each object $A \in \mathcal A$, choose an injective resolution \begin{align*} 0 \longrightarrow A \xrightarrow{\eta_A} I_A^0 \xrightarrow{d_A^0} I_A^1 \xrightarrow{d_A^1} I_A^2 \xrightarrow{d_A^2} \cdots . \end{align*} Thus each $I_A^n$ is injective, $\eta_A$ is a monomorphism, and the augmented complex is exact. Since $F$ is additive, applying $F$ to the nonnegative part $I_A^\bullet$ gives a cochain complex in $\mathcal B$: \begin{align*} F(I_A^0) \xrightarrow{F(d_A^0)} F(I_A^1) \xrightarrow{F(d_A^1)} F(I_A^2) \xrightarrow{F(d_A^2)} \cdots , \end{align*} because $d_A^{n+1} \circ d_A^n = 0$ implies \begin{align*} F(d_A^{n+1}) \circ F(d_A^n) = F(d_A^{n+1} \circ d_A^n) = F(0) = 0. \end{align*} For each integer $i \geq 0$, define \begin{align*} R^iF(A) := H^i(F(I_A^\bullet)). \end{align*} This object exists because $\mathcal B$ is abelian, so kernels, images, and quotient objects exist. [/step] [step:Lift a morphism to a cochain map between injective resolutions] Let $f: A \to A'$ be a morphism in $\mathcal A$. Write the chosen injective resolutions of $A$ and $A'$ as \begin{align*} 0 \longrightarrow A \xrightarrow{\eta_A} I_A^0 \xrightarrow{d_A^0} I_A^1 \xrightarrow{d_A^1} I_A^2 \longrightarrow \cdots \end{align*} and \begin{align*} 0 \longrightarrow A' \xrightarrow{\eta_{A'}} I_{A'}^0 \xrightarrow{d_{A'}^0} I_{A'}^1 \xrightarrow{d_{A'}^1} I_{A'}^2 \longrightarrow \cdots . \end{align*} We construct morphisms \begin{align*} f^n: I_A^n \longrightarrow I_{A'}^n \end{align*} for all $n \geq 0$ such that \begin{align*} f^0 \circ \eta_A &= \eta_{A'} \circ f, \\ d_{A'}^n \circ f^n &= f^{n+1} \circ d_A^n \qquad \text{for all } n \geq 0. \end{align*} Since $I_{A'}^0$ is injective and $\eta_A: A \to I_A^0$ is a monomorphism, the morphism $\eta_{A'} \circ f: A \to I_{A'}^0$ extends across $\eta_A$. Hence there exists $f^0: I_A^0 \to I_{A'}^0$ with \begin{align*} f^0 \circ \eta_A = \eta_{A'} \circ f. \end{align*} Assume $f^0,\dots,f^n$ have been constructed and satisfy the cochain condition through degree $n-1$. Define $Z_A^{n+1} := \ker(d_A^{n+1})$ and $Z_{A'}^{n+1} := \ker(d_{A'}^{n+1})$, with inclusions \begin{align*} \iota_A^{n+1}: Z_A^{n+1} \longrightarrow I_A^{n+1}, \qquad \iota_{A'}^{n+1}: Z_{A'}^{n+1} \longrightarrow I_{A'}^{n+1}. \end{align*} Exactness of the injective resolutions gives \begin{align*} \operatorname{im}(d_A^n) = Z_A^{n+1}, \qquad \operatorname{im}(d_{A'}^n) = Z_{A'}^{n+1}. \end{align*} The equality $d_{A'}^n \circ f^n \circ d_A^{n-1} = f^{n+1} \circ d_A^n \circ d_A^{n-1} = 0$ in the already constructed range, with the evident interpretation when $n=0$, shows that $d_{A'}^n \circ f^n$ factors through $Z_A^{n+1}$. Since $Z_{A'}^{n+1} = \ker(d_{A'}^{n+1})$, the morphism obtained lands in $Z_{A'}^{n+1}$. Composing with the monomorphism $\iota_{A'}^{n+1}: Z_{A'}^{n+1} \to I_{A'}^{n+1}$ gives a morphism from $Z_A^{n+1}$ to the injective object $I_{A'}^{n+1}$. Now $\iota_A^{n+1}: Z_A^{n+1} \to I_A^{n+1}$ is a monomorphism. Since $I_{A'}^{n+1}$ is injective, the morphism $Z_A^{n+1} \to I_{A'}^{n+1}$ extends across $\iota_A^{n+1}$. Choose such an extension and call it \begin{align*} f^{n+1}: I_A^{n+1} \longrightarrow I_{A'}^{n+1}. \end{align*} By construction it satisfies \begin{align*} f^{n+1} \circ d_A^n = d_{A'}^n \circ f^n. \end{align*} Induction gives a cochain map $f^\bullet: I_A^\bullet \to I_{A'}^\bullet$ lifting $f$. [/step] [step:Show that different lifted cochain maps induce the same cohomology maps] Let $f^\bullet,g^\bullet: I_A^\bullet \to I_{A'}^\bullet$ be two cochain maps lifting the same morphism $f: A \to A'$. We prove that $f^\bullet$ and $g^\bullet$ are cochain homotopic. Define \begin{align*} u^n := f^n - g^n: I_A^n \longrightarrow I_{A'}^n \end{align*} for each $n \geq 0$. Then $u^\bullet$ is a cochain map and \begin{align*} u^0 \circ \eta_A = 0. \end{align*} We construct morphisms \begin{align*} s^{n+1}: I_A^{n+1} \longrightarrow I_{A'}^n \end{align*} for $n \geq -1$, with $s^0: I_A^0 \to 0$ interpreted as the zero morphism, such that \begin{align*} u^n = d_{A'}^{n-1} \circ s^n + s^{n+1} \circ d_A^n \end{align*} for every $n \geq 0$, where $d_{A'}^{-1}: A' \to I_{A'}^0$ means $\eta_{A'}$ and the term $d_{A'}^{-1} \circ s^0$ is zero. For $n=0$, the relation $u^0 \circ \eta_A = 0$ implies that $u^0$ vanishes on $\operatorname{im}(\eta_A) = \ker(d_A^0)$. Hence $u^0$ factors through $\operatorname{im}(d_A^0) = \ker(d_A^1)$. Since $I_{A'}^0$ is injective and $\ker(d_A^1) \to I_A^1$ is a monomorphism, this factor extends to a morphism \begin{align*} s^1: I_A^1 \longrightarrow I_{A'}^0 \end{align*} satisfying \begin{align*} s^1 \circ d_A^0 = u^0. \end{align*} Assume $s^1,\dots,s^n$ have been constructed so that the homotopy identity holds in degrees $0,\dots,n-1$. Define \begin{align*} v^n := u^n - d_{A'}^{n-1} \circ s^n: I_A^n \longrightarrow I_{A'}^n. \end{align*} The inductive hypothesis and the cochain-map identity for $u^\bullet$ imply \begin{align*} v^n \circ d_A^{n-1} &= u^n \circ d_A^{n-1} - d_{A'}^{n-1} \circ s^n \circ d_A^{n-1} \\ &= d_{A'}^{n-1} \circ u^{n-1} - d_{A'}^{n-1} \circ \bigl(u^{n-1} - d_{A'}^{n-2} \circ s^{n-1}\bigr) \\ &= d_{A'}^{n-1} \circ d_{A'}^{n-2} \circ s^{n-1} \\ &= 0. \end{align*} Thus $v^n$ vanishes on $\operatorname{im}(d_A^{n-1}) = \ker(d_A^n)$, so it factors through $\operatorname{im}(d_A^n) = \ker(d_A^{n+1})$. Since $I_{A'}^n$ is injective and $\ker(d_A^{n+1}) \to I_A^{n+1}$ is a monomorphism, this factor extends to a morphism \begin{align*} s^{n+1}: I_A^{n+1} \longrightarrow I_{A'}^n \end{align*} with \begin{align*} s^{n+1} \circ d_A^n = v^n. \end{align*} Equivalently, \begin{align*} u^n = d_{A'}^{n-1} \circ s^n + s^{n+1} \circ d_A^n. \end{align*} Hence $f^\bullet$ and $g^\bullet$ are cochain homotopic. Applying the additive functor $F$ gives cochain homotopic maps of complexes \begin{align*} F(f^\bullet),F(g^\bullet): F(I_A^\bullet) \longrightarrow F(I_{A'}^\bullet). \end{align*} Cochain homotopic maps induce the same morphism on cohomology by the defining formula for a homotopy: if $z \in \ker F(d_A^i)$ represents a cohomology class, then \begin{align*} F(f^i)(z) - F(g^i)(z) = F(d_{A'}^{i-1})F(s^i)(z) + F(s^{i+1})F(d_A^i)(z) = F(d_{A'}^{i-1})F(s^i)(z), \end{align*} so the difference is a boundary. Therefore the induced morphism on $H^i$ is independent of the chosen lift. [/step] [step:Define the morphism maps and verify functoriality] For a morphism $f: A \to A'$ in $\mathcal A$, choose any lifted cochain map \begin{align*} f^\bullet: I_A^\bullet \longrightarrow I_{A'}^\bullet \end{align*} and define \begin{align*} R^iF(f) := H^i(F(f^\bullet)): R^iF(A) \longrightarrow R^iF(A'). \end{align*} The previous step shows that this definition is independent of the chosen lift. Let $\operatorname{id}_A: A \to A$ be the identity morphism. The identity cochain map \begin{align*} \operatorname{id}_{I_A^\bullet}: I_A^\bullet \longrightarrow I_A^\bullet \end{align*} lifts $\operatorname{id}_A$, so \begin{align*} R^iF(\operatorname{id}_A) = H^i(F(\operatorname{id}_{I_A^\bullet})) = \operatorname{id}_{H^i(F(I_A^\bullet))} = \operatorname{id}_{R^iF(A)}. \end{align*} Let $f: A \to A'$ and $g: A' \to A''$ be morphisms in $\mathcal A$. Choose lifted cochain maps \begin{align*} f^\bullet: I_A^\bullet \longrightarrow I_{A'}^\bullet, \qquad g^\bullet: I_{A'}^\bullet \longrightarrow I_{A''}^\bullet. \end{align*} Then $g^\bullet \circ f^\bullet$ is a lifted cochain map for $g \circ f$. Hence \begin{align*} R^iF(g \circ f) &= H^i(F(g^\bullet \circ f^\bullet)) \\ &= H^i(F(g^\bullet) \circ F(f^\bullet)) \\ &= H^i(F(g^\bullet)) \circ H^i(F(f^\bullet)) \\ &= R^iF(g) \circ R^iF(f). \end{align*} Thus $R^iF: \mathcal A \to \mathcal B$ is a functor for every $i \geq 0$. Since $F$ is additive and cohomology is additive on morphisms of complexes, $R^iF$ is additive. [/step] [step:Identify the zeroth derived functor with the original functor] Fix an object $A \in \mathcal A$. The beginning of the injective resolution is exact: \begin{align*} 0 \longrightarrow A \xrightarrow{\eta_A} I_A^0 \xrightarrow{d_A^0} I_A^1. \end{align*} Since $F$ is left exact, the sequence \begin{align*} 0 \longrightarrow F(A) \xrightarrow{F(\eta_A)} F(I_A^0) \xrightarrow{F(d_A^0)} F(I_A^1) \end{align*} is exact in $\mathcal B$. Therefore $F(\eta_A)$ identifies $F(A)$ with the kernel of $F(d_A^0)$. By definition, \begin{align*} R^0F(A) = H^0(F(I_A^\bullet)) = \ker(F(d_A^0)). \end{align*} Thus $F(\eta_A)$ induces an isomorphism \begin{align*} F(A) \xrightarrow{\sim} R^0F(A). \end{align*} This isomorphism is natural in $A$. Indeed, for a morphism $f: A \to A'$ and a lifted cochain map $f^\bullet: I_A^\bullet \to I_{A'}^\bullet$, the defining lifting equation gives \begin{align*} f^0 \circ \eta_A = \eta_{A'} \circ f. \end{align*} Applying $F$ and passing to kernels gives the commutative square \begin{align*} F(f) \text{ followed by } F(\eta_{A'}) = F(\eta_A) \text{ followed by } H^0(F(f^\bullet)). \end{align*} Equivalently, the family of isomorphisms $F(A) \xrightarrow{\sim} R^0F(A)$ is natural. Hence $R^0F \cong F$. [/step] [step:Prove independence from the chosen injective resolutions] Let $J_A^\bullet$ be another choice of injective resolution for each object $A \in \mathcal A$, and let $\widetilde{R}^iF(A) := H^i(F(J_A^\bullet))$ be the functors obtained from this second choice. For each $A$, apply the lifting construction to the identity morphism $\operatorname{id}_A: A \to A$ to obtain cochain maps \begin{align*} \alpha_A^\bullet: I_A^\bullet \longrightarrow J_A^\bullet, \qquad \beta_A^\bullet: J_A^\bullet \longrightarrow I_A^\bullet \end{align*} lifting $\operatorname{id}_A$. The composites $\beta_A^\bullet \circ \alpha_A^\bullet$ and $\operatorname{id}_{I_A^\bullet}$ are both lifts of $\operatorname{id}_A$ to $I_A^\bullet$. By the homotopy uniqueness step, they are cochain homotopic, and hence induce the same morphism on cohomology. Similarly, $\alpha_A^\bullet \circ \beta_A^\bullet$ and $\operatorname{id}_{J_A^\bullet}$ induce the same morphism on cohomology. Therefore \begin{align*} H^i(F(\alpha_A^\bullet)): R^iF(A) \longrightarrow \widetilde{R}^iF(A) \end{align*} is an isomorphism with inverse $H^i(F(\beta_A^\bullet))$. These isomorphisms are natural in $A$. For a morphism $f: A \to A'$, both paths around the naturality square are induced by lifted cochain maps from $I_A^\bullet$ to $J_{A'}^\bullet$ lifting the same morphism $f$. The homotopy uniqueness step implies that the two induced morphisms on cohomology agree. Hence the two choices of injective resolutions produce naturally isomorphic functors. Combining the construction of $R^iF$, the functoriality verification, the natural identification $R^0F \cong F$, and the natural independence of choices proves the theorem. [/step]