let G, H be Group; :: thesis: for g being Homomorphism of G,H holds
( G ./. (Ker g), Image g are_isomorphic & ex h being Homomorphism of (G ./. (Ker g)),(Image g) st
( h is bijective & g = h * (nat_hom (Ker g)) ) )
let g be Homomorphism of G,H; :: thesis: ( G ./. (Ker g), Image g are_isomorphic & ex h being Homomorphism of (G ./. (Ker g)),(Image g) st
( h is bijective & g = h * (nat_hom (Ker g)) ) )
set I = G ./. (Ker g);
set J = Image g;
defpred S₁[ set , set ] means for a being Element of G st $1 = a * (Ker g) holds
$2 = g . a;
A1: dom (nat_hom (Ker g)) = the carrier of G by FUNCT_2:def 1;
A2: for S being Element of (G ./. (Ker g)) ex T being Element of (Image g) st S₁[S,T]

proof

let S be Element of (G ./. (Ker g)); :: thesis: ex T being Element of (Image g) st S₁[S,T]
consider a being Element of G such that
A3: S = a * (Ker g) and
S = (Ker g) * a by Th13;
g . a in Image g by Th45;
then reconsider T = g . a as Element of (Image g) ;
take T ; :: thesis: S₁[S,T]
let b be Element of G; :: thesis: ( S = b * (Ker g) implies T = g . b )
assume S = b * (Ker g) ; :: thesis: T = g . b
then (a ") * b in Ker g by A3, GROUP_2:114;
then 1_ H = g . ((a ") * b) by Th41
.= (g . (a ")) * (g . b) by Def6
.= ((g . a) ") * (g . b) by Th32 ;
then g . b = ((g . a) ") " by GROUP_1:12;
hence T = g . b ; :: thesis: verum

end;

consider f being Function of (G ./. (Ker g)),(Image g) such that
A4: for S being Element of (G ./. (Ker g)) holds S₁[S,f . S] from FUNCT_2:sch 3(A2);

now :: thesis: for S, T being Element of (G ./. (Ker g)) holds f . (S * T) = (f . S) * (f . T)

let S, T be Element of (G ./. (Ker g)); :: thesis: f . (S * T) = (f . S) * (f . T)
consider a being Element of G such that
A5: S = a * (Ker g) and
S = (Ker g) * a by Th13;
consider b being Element of G such that
A6: T = b * (Ker g) and
A7: T = (Ker g) * b by Th13;
A8: f . T = g . b by A4, A6;
f . S = g . a by A4, A5;
then A9: (f . S) * (f . T) = (g . a) * (g . b) by A8, GROUP_2:43
.= g . (a * b) by Def6 ;
S * T = (a * (Ker g)) * ((Ker g) * b) by A5, A7, Def3
.= ((a * (Ker g)) * (Ker g)) * b by GROUP_3:11
.= (a * (Ker g)) * b by Th5
.= a * ((Ker g) * b) by GROUP_2:106
.= a * (b * (Ker g)) by GROUP_3:117
.= (a * b) * (Ker g) by GROUP_2:105 ;
hence f . (S * T) = (f . S) * (f . T) by A4, A9; :: thesis: verum

end;

then reconsider f = f as Homomorphism of (G ./. (Ker g)),(Image g) by Def6;
A10: f is one-to-one

proof

let y1, y2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not y1 in dom f or not y2 in dom f or not f . y1 = f . y2 or y1 = y2 )
assume ( y1 in dom f & y2 in dom f ) ; :: thesis: ( not f . y1 = f . y2 or y1 = y2 )
then reconsider S = y1, T = y2 as Element of (G ./. (Ker g)) ;
assume A11: f . y1 = f . y2 ; :: thesis: y1 = y2
consider a being Element of G such that
A12: S = a * (Ker g) and
S = (Ker g) * a by Th13;
consider b being Element of G such that
A13: T = b * (Ker g) and
T = (Ker g) * b by Th13;
A14: f . T = g . b by A4, A13;
f . S = g . a by A4, A12;
then ((g . b) ") * (g . a) = 1_ H by A11, A14, GROUP_1:def 5;
then 1_ H = (g . (b ")) * (g . a) by Th32
.= g . ((b ") * a) by Def6 ;
then (b ") * a in Ker g by Th41;
hence y1 = y2 by A12, A13, GROUP_2:114; :: thesis: verum

end;

A15: dom g = the carrier of G by FUNCT_2:def 1;

A16: now :: thesis: for x being object holds
( ( x in dom g implies ( x in dom (nat_hom (Ker g)) & (nat_hom (Ker g)) . x in dom f ) ) & ( x in dom (nat_hom (Ker g)) & (nat_hom (Ker g)) . x in dom f implies x in dom g ) )

let x be object ; :: thesis: ( ( x in dom g implies ( x in dom (nat_hom (Ker g)) & (nat_hom (Ker g)) . x in dom f ) ) & ( x in dom (nat_hom (Ker g)) & (nat_hom (Ker g)) . x in dom f implies x in dom g ) )
thus ( x in dom g implies ( x in dom (nat_hom (Ker g)) & (nat_hom (Ker g)) . x in dom f ) ) :: thesis: ( x in dom (nat_hom (Ker g)) & (nat_hom (Ker g)) . x in dom f implies x in dom g )

proof

assume A17: x in dom g ; :: thesis: ( x in dom (nat_hom (Ker g)) & (nat_hom (Ker g)) . x in dom f )
hence x in dom (nat_hom (Ker g)) by A1; :: thesis: (nat_hom (Ker g)) . x in dom f
A18: dom f = the carrier of (G ./. (Ker g)) by FUNCT_2:def 1;
(nat_hom (Ker g)) . x in rng (nat_hom (Ker g)) by A1, A17, FUNCT_1:def 3;
hence (nat_hom (Ker g)) . x in dom f by A18; :: thesis: verum

end;

assume that
A19: x in dom (nat_hom (Ker g)) and
(nat_hom (Ker g)) . x in dom f ; :: thesis: x in dom g
thus x in dom g by A15, A19; :: thesis: verum

end;

the carrier of (Image g) c= rng f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (Image g) or x in rng f )
assume x in the carrier of (Image g) ; :: thesis: x in rng f
then x in Image g ;
then consider a being Element of G such that
A20: x = g . a by Th45;
reconsider S = a * (Ker g) as Element of (G ./. (Ker g)) by Th14;
( f . S = g . a & the carrier of (G ./. (Ker g)) = dom f ) by A4, FUNCT_2:def 1;
hence x in rng f by A20, FUNCT_1:def 3; :: thesis: verum

end;

then A21: rng f = the carrier of (Image g) ;
then f is bijective by A10, FUNCT_2:def 3;
hence G ./. (Ker g), Image g are_isomorphic ; :: thesis: ex h being Homomorphism of (G ./. (Ker g)),(Image g) st
( h is bijective & g = h * (nat_hom (Ker g)) )
take f ; :: thesis: ( f is bijective & g = f * (nat_hom (Ker g)) )
thus f is bijective by A21, A10, FUNCT_2:def 3; :: thesis: g = f * (nat_hom (Ker g))

now :: thesis: for x being object st x in dom g holds
g . x = f . ((nat_hom (Ker g)) . x)

let x be object ; :: thesis: ( x in dom g implies g . x = f . ((nat_hom (Ker g)) . x) )
assume x in dom g ; :: thesis: g . x = f . ((nat_hom (Ker g)) . x)
then reconsider a = x as Element of G ;
(nat_hom (Ker g)) . a = a * (Ker g) by Def8;
hence g . x = f . ((nat_hom (Ker g)) . x) by A4; :: thesis: verum

end;

hence g = f * (nat_hom (Ker g)) by A16, FUNCT_1:10; :: thesis: verum