Corollary

Tag 0DTZ, permanent. Cite it as [Bourbaki, Tag 0DTZ].

Let $(e, E)$ and $(e', E')$ be two injective resolutions of N; there exists a morphism $\alpha : E \to E'$ and only one up to homotopy such that $\alpha \circ e = e'$ .

Bourbaki puts the proof directly after the statement, so what is above is the statement and its proof together.