set H = multMagma(# the carrier of N,the multF of N #);
reconsider H = multMagma(# the carrier of N,the multF of N #) as strict normal Subgroup of G by Lm7;
set IT = nat_hom H;
reconsider K = G ./. N as GroupWithOperators of O ;
Cosets H = Cosets N by Def14;
then reconsider IT' = nat_hom H as Function of G,K ;

A1: now

let a, b be Element of G; :: thesis: IT' . (a * b) = (IT' . a) * (IT' . b)
IT' . (a * b) = ((nat_hom H) . a) * ((nat_hom H) . b) by GROUP_6:def 7
.= (IT' . a) * (IT' . b) by Def15 ;
hence IT' . (a * b) = (IT' . a) * (IT' . b) ; :: thesis: verum

end;

now

let o be Element of O; :: thesis: for g being Element of G holds IT' . ((G ^ b₂) . b₃) = (K ^ b₂) . (IT' . b₃)
let g be Element of G; :: thesis: IT' . ((G ^ b₁) . b₂) = (K ^ b₁) . (IT' . b₂)

per cases ( O <> {} or O = {} ) ;

suppose A2: O <> {} ; :: thesis: IT' . ((G ^ b₁) . b₂) = (K ^ b₁) . (IT' . b₂)

then the action of K . o in Funcs the carrier of K,the carrier of K by FUNCT_2:7;
then consider f being Function such that
A3: ( f = the action of K . o & dom f = the carrier of K & rng f c= the carrier of K ) by FUNCT_2:def 2;
A4: (K ^ o) . (IT' . g) = f . (IT' . g) by A2, A3, Def6;
A5: f = { [A,B] where A, B is Element of Cosets N : ex g, h being Element of G st
( g in A & h in B & h = (G ^ o) . g ) } by A2, A3, Def16;
[(IT' . g),(f . (IT' . g))] in f by A3, FUNCT_1:def 4;
then consider A, B being Element of Cosets N such that
A6: ( [(IT' . g),(f . (IT' . g))] = [A,B] & ex g, h being Element of G st
( g in A & h in B & h = (G ^ o) . g ) ) by A5;
A7: ( IT' . g = A & f . (IT' . g) = B ) by A6, ZFMISC_1:33;
consider g', h' being Element of G such that
A8: ( g' in A & h' in B & h' = (G ^ o) . g' ) by A6;
reconsider A = A, B = B as Element of Cosets H by Def14;
( A = g' * H & B = h' * H ) by A8, Lm9;
then g * H = g' * H by A7, GROUP_6:def 9;
then (g' " ) * g in H by GROUP_2:137;
then (g' " ) * g in the carrier of N by STRUCT_0:def 5;
then (g' " ) * g in N by STRUCT_0:def 5;
then (G ^ o) . ((g' " ) * g) in N by Lm10;
then (G ^ o) . ((g' " ) * g) in the carrier of N by STRUCT_0:def 5;
then A9: (G ^ o) . ((g' " ) * g) in H by STRUCT_0:def 5;
A10: (G ^ o) . ((g' " ) * g) = ((G ^ o) . (g' " )) * ((G ^ o) . g) by GROUP_6:def 7
.= (((G ^ o) . g') " ) * ((G ^ o) . g) by GROUP_6:41 ;
IT' . ((G ^ o) . g) = ((G ^ o) . g) * H by GROUP_6:def 9
.= ((G ^ o) . g') * H by A9, A10, GROUP_2:137
.= B by A8, Lm9 ;
hence IT' . ((G ^ o) . g) = (K ^ o) . (IT' . g) by A4, A6, ZFMISC_1:33; :: thesis: verum

end;

suppose O = {} ; :: thesis: IT' . ((G ^ b₁) . b₂) = (K ^ b₁) . (IT' . b₂)

then ( G ^ o = id the carrier of G & K ^ o = id the carrier of K ) by Def6;
then ( (G ^ o) . g = g & (K ^ o) . (IT' . g) = IT' . g ) by FUNCT_1:35;
hence IT' . ((G ^ o) . g) = (K ^ o) . (IT' . g) ; :: thesis: verum

end;

end;

end;

then reconsider IT' = IT' as Homomorphism of G,K by A1, Def18, GROUP_6:def 7;
reconsider IT' = IT' as Homomorphism of G,(G ./. N) ;
take IT' ; :: thesis: for H being strict normal Subgroup of G st H = multMagma(# the carrier of N,the multF of N #) holds
IT' = nat_hom H
let H be strict normal Subgroup of G; :: thesis: ( H = multMagma(# the carrier of N,the multF of N #) implies IT' = nat_hom H )
assume H = multMagma(# the carrier of N,the multF of N #) ; :: thesis: IT' = nat_hom H
hence IT' = nat_hom H ; :: thesis: verum