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 for a, b being Element of G holds IT9 . (a * b) = (IT9 . a) * (IT9 . b)end;
now 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;
for g being Element of G holds IT9 . ((G ^ b2) . b3) = (K ^ b2) . (IT9 . b3)let g be
Element of
G;
IT9 . ((G ^ b1) . b2) = (K ^ b1) . (IT9 . b2)per cases
( O <> {} or O = {} )
;
suppose A2:
O <> {}
;
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 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;
verum 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
; 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; ( 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 #)
; IT9 = nat_hom H
hence
IT9 = nat_hom H
; verum