let G1, G2 be Group; :: thesis: 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)
let N be normal Subgroup of G1; :: thesis: 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)
let f be Homomorphism of G1,G2; :: thesis: ( N is Subgroup of Ker f implies ex fBar being Homomorphism of (G1 ./. N),G2 st f = fBar * (nat_hom N) )
assume A1: N is Subgroup of Ker f ; :: thesis: ex fBar being Homomorphism of (G1 ./. N),G2 st f = fBar * (nat_hom N)
defpred S₁[ Element of (G1 ./. N), Element of G2] means ex g being Element of G1 st
( $1 = g * N & $2 = f . g );
A2: for x being Element of (G1 ./. N) ex y being Element of G2 st S₁[x,y]

proof

let x be Element of (G1 ./. N); :: thesis: ex y being Element of G2 st S₁[x,y]
x in G1 ./. N ;
then consider g1 being Element of G1 such that
B1: ( x = g1 * N & x = N * g1 ) by GROUP_6:23;
consider y being Element of G2 such that
B2: y = f . g1 ;
take y ; :: thesis: S₁[x,y]
thus S₁[x,y] by B1, B2; :: thesis: verum

end;

consider fBar being Function of (G1 ./. N),G2 such that
A3: for x being Element of (G1 ./. N) holds S₁[x,fBar . x] from FUNCT_2:sch 3(A2);
for x1, x2 being Element of (G1 ./. N) holds fBar . (x1 * x2) = (fBar . x1) * (fBar . x2)

proof

let x1, x2 be Element of (G1 ./. N); :: thesis: fBar . (x1 * x2) = (fBar . x1) * (fBar . x2)
consider g12 being Element of G1 such that
B1: ( x1 * x2 = g12 * N & fBar . (x1 * x2) = f . g12 ) by A3;
consider g1 being Element of G1 such that
B2: ( x1 = g1 * N & fBar . x1 = f . g1 ) by A3;
consider g2 being Element of G1 such that
B3: ( x2 = g2 * N & fBar . x2 = f . g2 ) by A3;
B4: ( (nat_hom N) . g1 = x1 & (nat_hom N) . g2 = x2 ) by B2, B3, GROUP_6:def 8;
(g1 * g2) * N = (nat_hom N) . (g1 * g2) by GROUP_6:def 8
.= g12 * N by B1, B4, GROUP_6:def 6 ;
then consider n being Element of G1 such that
B5: ( n in N & g12 = (g1 * g2) * n ) by Th52;
f . g12 = (f . (g1 * g2)) * (f . n) by B5, GROUP_6:def 6
.= (f . (g1 * g2)) * (1_ G2) by A1, B5, GROUP_2:40, GROUP_6:41
.= f . (g1 * g2) by GROUP_1:def 4
.= (f . g1) * (f . g2) by GROUP_6:def 6 ;
hence fBar . (x1 * x2) = (fBar . x1) * (fBar . x2) by B1, B2, B3; :: thesis: verum

end;

then reconsider fBar = fBar as Homomorphism of (G1 ./. N),G2 by GROUP_6:def 6;
take fBar ; :: thesis: f = fBar * (nat_hom N)
for g being Element of G1 holds f . g = (fBar * (nat_hom N)) . g

proof

let g be Element of G1; :: thesis: f . g = (fBar * (nat_hom N)) . g
consider g1 being Element of G1 such that
B1: ( (nat_hom N) . g = g1 * N & fBar . ((nat_hom N) . g) = f . g1 ) by A3;
g * N = g1 * N by B1, GROUP_6:def 8;
then consider n being Element of G1 such that
B2: ( n in N & g = g1 * n ) by Th52;
f . g = (f . g1) * (f . n) by B2, GROUP_6:def 6
.= (f . g1) * (1_ G2) by A1, B2, GROUP_2:40, GROUP_6:41
.= f . g1 by GROUP_1:def 4
.= (fBar * (nat_hom N)) . g by B1, FUNCT_2:15 ;
hence f . g = (fBar * (nat_hom N)) . g ; :: thesis: verum

end;

hence f = fBar * (nat_hom N) by FUNCT_2:def 8; :: thesis: verum