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 ;
reconsider IT' = nat_hom H as Function of G,K by Def14;

A1: now

let a, b be Element of ; :: 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 holds IT' . ((G ^ b₂) . b₃) = (K ^ b₂) . (IT' . b₃)
let g be Element of ; :: 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 and
A4: dom f = the carrier of K and
rng f c= the carrier of K by FUNCT_2:def 2;
A5: f = { [A,B] where A, B is Element of Cosets N : ex g, h being Element of st
( g in A & h in B & h = (G ^ o) . g ) } by A2, A3, Def16;
[(IT' . g),(f . (IT' . g))] in f by A4, FUNCT_1:def 4;
then consider A, B being Element of Cosets N such that
A6: [(IT' . g),(f . (IT' . g))] = [A,B] and
A7: ex g, h being Element of st
( g in A & h in B & h = (G ^ o) . g ) by A5;
A8: IT' . g = A by A6, ZFMISC_1:33;
consider g', h' being Element of such that
A9: g' in A and
A10: ( h' in B & h' = (G ^ o) . g' ) by A7;
A11: (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 ;
reconsider A = A, B = B as Element of Cosets H by Def14;
A = g' * H by A9, Lm9;
then g * H = g' * H by A8, 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 A12: (G ^ o) . ((g' " ) * g) in H by STRUCT_0:def 5;
A13: (K ^ o) . (IT' . g) = f . (IT' . g) by A2, A3, Def6;
IT' . ((G ^ o) . g) = ((G ^ o) . g) * H by GROUP_6:def 9
.= ((G ^ o) . g') * H by A12, A11, GROUP_2:137
.= B by A10, Lm9 ;
hence IT' . ((G ^ o) . g) = (K ^ o) . (IT' . g) by A13, A6, ZFMISC_1:33; :: thesis: verum

end;

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

then G ^ o = id the carrier of G by Def6;
then A15: (G ^ o) . g = g by FUNCT_1:35;
K ^ o = id the carrier of K by A14, Def6;
hence IT' . ((G ^ o) . g) = (K ^ o) . (IT' . g) by A15, FUNCT_1:35; :: 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