theorem UniversalPropertyQuotientGroups: :: GROUP_24:53

for G1, G2 being Group
for N being normal Subgroup of G1
for f being Homomorphism of G1,G2 st N is Subgroup of Ker f holds
ex fBar being Homomorphism of (G1 ./. N),G2 st f = fBar * (nat_hom N)