A note on the definition of derived functors

The purpose of this note is to consider in detail the construction of derived functors. The classical construction, such as in Cartan-Eilenberg or Grothendieck, is clarified, and it is shown, at the same time, that everything can be formalized in ZFC, unlike the approach using derived categories. Our work is done in a more general context in which the codomain of our functors is any Grothendieck category, not necessarily abelian groups.