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;

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

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;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

now :: thesis: for o being Element of O

for g being Element of G holds IT9 . ((G ^ o) . g) = (K ^ o) . (IT9 . g)

then reconsider IT9 = IT9 as Homomorphism of G,K by A1, Def18, GROUP_6:def 6;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_{2}) . b_{3}) = (K ^ b_{2}) . (IT9 . b_{3})

let g be Element of G; :: thesis: IT9 . ((G ^ b_{1}) . b_{2}) = (K ^ b_{1}) . (IT9 . b_{2})

end;let g be Element of G; :: thesis: IT9 . ((G ^ b

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

end;

suppose A2:
O <> {}
; :: thesis: IT9 . ((G ^ b_{1}) . b_{2}) = (K ^ b_{1}) . (IT9 . b_{2})

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;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

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