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) = (() . a) * (() . 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 ^ b2) . b3) = (K ^ b2) . (IT9 . b3)
let g be Element of G; :: thesis: IT9 . ((G ^ b1) . b2) = (K ^ b1) . (IT9 . b2)
per cases ( O <> {} or O = {} ) ;
suppose A2: O <> {} ; :: thesis: IT9 . ((G ^ b1) . b2) = (K ^ b1) . (IT9 . b2)
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 ;
[(IT9 . g),(f . (IT9 . g))] in f by ;
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 ;
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 ;
then g * H = g9 * H by ;
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
.= B by ;
hence IT9 . ((G ^ o) . g) = (K ^ o) . (IT9 . g) by ; :: thesis: verum
end;
suppose A14: O = {} ; :: thesis: IT9 . ((G ^ b1) . b2) = (K ^ b1) . (IT9 . b2)
then G ^ o = id the carrier of G by Def6;
then A15: (G ^ o) . g = g ;
K ^ o = id the carrier of K by ;
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 ;
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