coequalizer of modules

1. Proposition

with

note that 20240122-coequalizer_of_modules_b71e53a5c189bd6b8a86f0ba771ad9cff3dd7ffa.svg is a module homomorphism (see: Set of module homomorphisms as abelian group) Hence the module is a welldefined module

Let 20240122-coequalizer_of_modules_f033e8bc0590490e41c5828e661cf6c892da1117.svg such that . Then

Let 20240122-coequalizer_of_modules_1bfe7e289f13ae9ab51118624e48fbf3aefcf40d.svg be another module and

making this a cofork Then it follows, that

Thus 20240122-coequalizer_of_modules_16cc31348c3f80f01f2e901b53a39da6ff66367d.svg and by fundamental theorem of module homomorphisms, there exists a unique morphism