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 Lm6;
set IT = nat_hom H;
reconsider K = G ./. N as GroupWithOperators of O ;
reconsider IT9 = nat_hom H as Function of G,K by Def14;

A1: now :: thesis: for a, b being Element of G holds IT9 . (a * b) = (IT9 . a) * (IT9 . b)

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

end;

now :: thesis: for o being Element of O
for g being Element of G holds IT9 . ((G ^ o) . g) = (K ^ o) . (IT9 . g)

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

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

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

then the action of K . o in Funcs ( the carrier of K, the carrier of K) by FUNCT_2:5;
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 G st
( g in A & h in B & h = (G ^ o) . g ) } by A2, A3, Def16;
[(IT9 . g),(f . (IT9 . g))] in f by A4, FUNCT_1:def 2;
then consider A, B being Element of Cosets N such that
A6: [(IT9 . g),(f . (IT9 . g))] = [A,B] and
A7: ex g, h being Element of G st
( g in A & h in B & h = (G ^ o) . g ) by A5;
A8: IT9 . g = A by A6, XTUPLE_0:1;
consider g9, h9 being Element of G such that
A9: g9 in A and
A10: ( h9 in B & h9 = (G ^ o) . g9 ) by A7;
A11: (G ^ o) . ((g9 ") * g) = ((G ^ o) . (g9 ")) * ((G ^ o) . g) by GROUP_6:def 6
.= (((G ^ o) . g9) ") * ((G ^ o) . g) by GROUP_6:32 ;
reconsider A = A, B = B as Element of Cosets H by Def14;
A = g9 * H by A9, Lm8;
then g * H = g9 * H by A8, GROUP_6:def 8;
then (g9 ") * g in H by GROUP_2:114;
then (g9 ") * g in the carrier of N by STRUCT_0:def 5;
then (g9 ") * g in N by STRUCT_0:def 5;
then (G ^ o) . ((g9 ") * g) in N by Lm9;
then (G ^ o) . ((g9 ") * g) in the carrier of N by STRUCT_0:def 5;
then A12: (G ^ o) . ((g9 ") * g) in H by STRUCT_0:def 5;
A13: (K ^ o) . (IT9 . g) = f . (IT9 . g) by A2, A3, Def6;
IT9 . ((G ^ o) . g) = ((G ^ o) . g) * H by GROUP_6:def 8
.= ((G ^ o) . g9) * H by A12, A11, GROUP_2:114
.= B by A10, Lm8 ;
hence IT9 . ((G ^ o) . g) = (K ^ o) . (IT9 . g) by A13, A6, XTUPLE_0:1; :: thesis: verum

end;

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

then G ^ o = id the carrier of G by Def6;
then A15: (G ^ o) . g = g ;
K ^ o = id the carrier of K by A14, Def6;
hence IT9 . ((G ^ o) . g) = (K ^ o) . (IT9 . g) by A15; :: thesis: verum

end;

end;

end;

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