reconsider H = multMagma(# the carrier of N, the multF of N #) as strict normal Subgroup of G by Lm6;
set G9 = multMagma(# the carrier of (G ./. N), the multF of (G ./. N) #);
A1: now :: thesis: ex e being Element of (G ./. N) st
for h being Element of (G ./. N) holds
( h * e = h & e * h = h & ex g being Element of (G ./. N) st
( h * g = e & g * h = e ) )
set e9 = 1_ (G ./. H);
reconsider e = 1_ (G ./. H) as Element of (G ./. N) by Def14;
take e = e; :: thesis: for h being Element of (G ./. N) holds
( h * e = h & e * h = h & ex g being Element of (G ./. N) st
( h * g = e & g * h = e ) )

let h be Element of (G ./. N); :: thesis: ( h * e = h & e * h = h & ex g being Element of (G ./. N) st
( h * g = e & g * h = e ) )

reconsider h9 = h as Element of (G ./. H) by Def14;
set g = h9 " ;
set g9 = h9 " ;
h * e = h9 * (1_ (G ./. H)) by Def15
.= h9 by GROUP_1:def 4 ;
hence h * e = h ; :: thesis: ( e * h = h & ex g being Element of (G ./. N) st
( h * g = e & g * h = e ) )

e * h = (1_ (G ./. H)) * h9 by Def15
.= h9 by GROUP_1:def 4 ;
hence e * h = h ; :: thesis: ex g being Element of (G ./. N) st
( h * g = e & g * h = e )

reconsider g = h9 " as Element of (G ./. N) by Def14;
take g = g; :: thesis: ( h * g = e & g * h = e )
h * g = h9 * (h9 ") by Def15
.= 1_ (G ./. H) by GROUP_1:def 5 ;
hence h * g = e ; :: thesis: g * h = e
g * h = (h9 ") * h9 by Def15
.= 1_ (G ./. H) by GROUP_1:def 5 ;
hence g * h = e ; :: thesis: verum
end;
A2: now :: thesis: for G9 being Group
for a being Action of O, the carrier of G9 st a = the action of (G ./. N) & multMagma(# the carrier of G9, the multF of G9 #) = multMagma(# the carrier of (G ./. N), the multF of (G ./. N) #) holds
a is distributive
let G9 be Group; :: thesis: for a being Action of O, the carrier of G9 st a = the action of (G ./. N) & multMagma(# the carrier of G9, the multF of G9 #) = multMagma(# the carrier of (G ./. N), the multF of (G ./. N) #) holds
a is distributive

let a be Action of O, the carrier of G9; :: thesis: ( a = the action of (G ./. N) & multMagma(# the carrier of G9, the multF of G9 #) = multMagma(# the carrier of (G ./. N), the multF of (G ./. N) #) implies a is distributive )
assume A3: a = the action of (G ./. N) ; :: thesis: ( multMagma(# the carrier of G9, the multF of G9 #) = multMagma(# the carrier of (G ./. N), the multF of (G ./. N) #) implies a is distributive )
assume A4: multMagma(# the carrier of G9, the multF of G9 #) = multMagma(# the carrier of (G ./. N), the multF of (G ./. N) #) ; :: thesis: a is distributive
now :: thesis: for o being Element of O st o in O holds
a . o is Homomorphism of G9,G9
let o be Element of O; :: thesis: ( o in O implies a . o is Homomorphism of G9,G9 )
assume A5: o in O ; :: thesis: a . o is Homomorphism of G9,G9
then A6: a . o = { [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 ;
a . o in Funcs ((),()) by ;
then consider f being Function such that
A7: a . o = f and
A8: dom f = Cosets N and
A9: rng f c= Cosets N by FUNCT_2:def 2;
reconsider f = f as Function of the carrier of G9, the carrier of G9 by ;
now :: thesis: for A1, A2 being Element of G9 holds f . (A1 * A2) = (f . A1) * (f . A2)
let A1, A2 be Element of G9; :: thesis: f . (A1 * A2) = (f . A1) * (f . A2)
set A3 = A1 * A2;
set B1 = f . A1;
set B2 = f . A2;
set B3 = f . (A1 * A2);
[A1,(f . A1)] in f by ;
then consider A19, B19 being Element of Cosets N such that
A10: [A1,(f . A1)] = [A19,B19] and
A11: ex g1, h1 being Element of G st
( g1 in A19 & h1 in B19 & h1 = (G ^ o) . g1 ) by A6, A7;
[A2,(f . A2)] in f by ;
then consider A29, B29 being Element of Cosets N such that
A12: [A2,(f . A2)] = [A29,B29] and
A13: ex g2, h2 being Element of G st
( g2 in A29 & h2 in B29 & h2 = (G ^ o) . g2 ) by A6, A7;
[(A1 * A2),(f . (A1 * A2))] in f by ;
then consider A39, B39 being Element of Cosets N such that
A14: [(A1 * A2),(f . (A1 * A2))] = [A39,B39] and
A15: ex g3, h3 being Element of G st
( g3 in A39 & h3 in B39 & h3 = (G ^ o) . g3 ) by A6, A7;
consider g3, h3 being Element of G such that
A16: g3 in A39 and
A17: h3 in B39 and
A18: h3 = (G ^ o) . g3 by A15;
consider g2, h2 being Element of G such that
A19: g2 in A29 and
A20: h2 in B29 and
A21: h2 = (G ^ o) . g2 by A13;
consider g1, h1 being Element of G such that
A22: g1 in A19 and
A23: h1 in B19 and
A24: h1 = (G ^ o) . g1 by A11;
A25: ( @ (() . g1) = () . g1 & @ (() . g2) = () . g2 ) ;
A26: ( (nat_hom H) . g1 = g1 * H & () . g2 = g2 * H ) by GROUP_6:def 8;
reconsider A19 = A19, A29 = A29, A39 = A39, B19 = B19, B29 = B29, B39 = B39 as Element of Cosets H by Def14;
A27: A29 = g2 * H by ;
A28: A39 = g3 * H by ;
A29: B29 = h2 * H by ;
reconsider A19 = A19, A29 = A29, B19 = B19, B29 = B29 as Element of (G ./. H) ;
A2 = g2 * H by ;
then A1 * A2 = the multF of G9 . (A19,A29) by
.= @ (A19 * A29) by
.= (@ A19) * (@ A29) by GROUP_6:20 ;
then A1 * A2 = (g1 * H) * (g2 * H) by
.= (() . g1) * (() . g2) by
.= () . (g1 * g2) by GROUP_6:def 6
.= (g1 * g2) * H by GROUP_6:def 8 ;
then g3 * H = (g1 * g2) * H by ;
then (g3 ") * (g1 * g2) in H by GROUP_2:114;
then (g3 ") * (g1 * g2) in the carrier of H by STRUCT_0:def 5;
then (g3 ") * (g1 * g2) in N by STRUCT_0:def 5;
then (G ^ o) . ((g3 ") * (g1 * g2)) in N by Lm9;
then ((G ^ o) . (g3 ")) * ((G ^ o) . (g1 * g2)) in N by GROUP_6:def 6;
then ((G ^ o) . (g3 ")) * (((G ^ o) . g1) * ((G ^ o) . g2)) in N by GROUP_6:def 6;
then (h3 ") * (h1 * h2) in N by ;
then (h3 ") * (h1 * h2) in the carrier of N by STRUCT_0:def 5;
then A30: (h3 ") * (h1 * h2) in H by STRUCT_0:def 5;
A31: ( (nat_hom H) . h1 = h1 * H & () . h2 = h2 * H ) by GROUP_6:def 8;
B39 = h3 * H by ;
then A32: f . (A1 * A2) = h3 * H by ;
A33: ( @ (() . h1) = () . h1 & @ (() . h2) = () . h2 ) ;
f . A2 = h2 * H by ;
then (f . A1) * (f . A2) = the multF of G9 . (B19,B29) by
.= @ (B19 * B29) by
.= (@ B19) * (@ B29) by GROUP_6:20 ;
then (f . A1) * (f . A2) = (h1 * H) * (h2 * H) by
.= (() . h1) * (() . h2) by
.= () . (h1 * h2) by GROUP_6:def 6
.= (h1 * h2) * H by GROUP_6:def 8 ;
hence f . (A1 * A2) = (f . A1) * (f . A2) by ; :: thesis: verum
end;
hence a . o is Homomorphism of G9,G9 by ; :: thesis: verum
end;
hence a is distributive ; :: thesis: verum
end;
the carrier of (G ./. N) = the carrier of (G ./. H) by Def14;
then A34: ( multMagma(# the carrier of (G ./. N), the multF of (G ./. N) #) is Group-like & multMagma(# the carrier of (G ./. N), the multF of (G ./. N) #) is associative ) by Def15;
now :: thesis: for x, y, z being Element of (G ./. N) holds (x * y) * z = x * (y * z)
let x, y, z be Element of (G ./. N); :: thesis: (x * y) * z = x * (y * z)
reconsider x9 = x, y9 = y, z9 = z as Element of multMagma(# the carrier of (G ./. N), the multF of (G ./. N) #) ;
( (x9 * y9) * z9 = (x * y) * z & x9 * (y9 * z9) = x * (y * z) ) ;
hence (x * y) * z = x * (y * z) by ; :: thesis: verum
end;
hence ( G ./. N is distributive & G ./. N is Group-like & G ./. N is associative ) by ; :: thesis: verum