let H, G 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: 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
A2: ( S = a * (Ker g) & S = (Ker g) * a ) by Th15;
g . a in Image g by Th54;
then reconsider T = g . a as Element of (Image g) by STRUCT_0:def 5;
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 A2, GROUP_2:137;
then 1_ H = g . ((a " ) * b) by Th50
.= (g . (a " )) * (g . b) by Def7
.= ((g . a) " ) * (g . b) by Th41 ;
then g . b = ((g . a) " ) " by GROUP_1:20;
hence T = g . b ; :: thesis: verum

end;

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

now

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
A4: S = a * (Ker g) and
S = (Ker g) * a by Th15;
consider b being Element of G such that
A5: T = b * (Ker g) and
A6: T = (Ker g) * b by Th15;
( f . S = g . a & f . T = g . b ) by A3, A4, A5;
then A7: (f . S) * (f . T) = (g . a) * (g . b) by GROUP_2:52
.= g . (a * b) by Def7 ;
S * T = (a * (Ker g)) * ((Ker g) * b) by A4, A6, Def4
.= ((a * (Ker g)) * (Ker g)) * b by GROUP_3:12
.= (a * (Ker g)) * b by Th6
.= a * ((Ker g) * b) by GROUP_2:128
.= a * (b * (Ker g)) by GROUP_3:140
.= (a * b) * (Ker g) by GROUP_2:127 ;
hence f . (S * T) = (f . S) * (f . T) by A3, A7; :: thesis: verum

end;

then reconsider f = f as Homomorphism of (G ./. (Ker g)),(Image g) by Def7;
the carrier of (Image g) c= rng f

proof

let x be set ; :: 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 by STRUCT_0:def 5;
then consider a being Element of G such that
A8: x = g . a by Th54;
reconsider S = a * (Ker g) as Element of (G ./. (Ker g)) by Th16;
( f . S = g . a & S in the carrier of (G ./. (Ker g)) & the carrier of (G ./. (Ker g)) = dom f ) by A3, FUNCT_2:def 1;
hence x in rng f by A8, FUNCT_1:def 5; :: thesis: verum

end;

then A9: rng f = the carrier of (Image g) by XBOOLE_0:def 10;
A10: f is one-to-one

proof

let y1 be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not y1 in dom f or not b₁ in dom f or not f . y1 = f . b₁ or y1 = b₁ )
let y2 be set ; :: 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)) ;
consider a being Element of G such that
A11: S = a * (Ker g) and
S = (Ker g) * a by Th15;
consider b being Element of G such that
A12: T = b * (Ker g) and
T = (Ker g) * b by Th15;
assume A13: f . y1 = f . y2 ; :: thesis: y1 = y2
( f . S = g . a & f . T = g . b ) by A3, A11, A12;
then ((g . b) " ) * (g . a) = 1_ H by A13, GROUP_1:def 6;
then 1_ H = (g . (b " )) * (g . a) by Th41
.= g . ((b " ) * a) by Def7 ;
then (b " ) * a in Ker g by Th50;
hence y1 = y2 by A11, A12, GROUP_2:137; :: thesis: verum

end;

then f is bijective by A9, Th70;
hence G ./. (Ker g), Image g are_isomorphic by Def15; :: 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)) )
A14: ( dom (nat_hom (Ker g)) = the carrier of G & dom g = the carrier of G ) by FUNCT_2:def 1;
thus f is bijective by A9, A10, Th70; :: thesis: g = f * (nat_hom (Ker g))

A15: now

let x be set ; :: 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 A16: 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 A14; :: thesis: (nat_hom (Ker g)) . x in dom f
( (nat_hom (Ker g)) . x in rng (nat_hom (Ker g)) & rng (nat_hom (Ker g)) c= the carrier of (G ./. (Ker g)) & dom f = the carrier of (G ./. (Ker g)) ) by A14, A16, FUNCT_1:def 5, FUNCT_2:def 1;
hence (nat_hom (Ker g)) . x in dom f ; :: thesis: verum

end;

assume ( x in dom (nat_hom (Ker g)) & (nat_hom (Ker g)) . x in dom f ) ; :: thesis: x in dom g
hence x in dom g by A14; :: thesis: verum

end;

now

let x be set ; :: 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 Def9;
hence g . x = f . ((nat_hom (Ker g)) . x) by A3; :: thesis: verum

end;

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