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

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;

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

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

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

the carrier of (G ./. N) = the carrier of (G ./. H)
by Def14;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

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

hence
a is distributive
; :: thesis: veruma . 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 A3, Def16;

a . o in Funcs ((Cosets N),(Cosets N)) by A3, A5, FUNCT_2:5;

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 A4, A8, A9, FUNCT_2:2;

end;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 A3, Def16;

a . o in Funcs ((Cosets N),(Cosets N)) by A3, A5, FUNCT_2:5;

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 A4, A8, A9, FUNCT_2:2;

now :: thesis: for A1, A2 being Element of G9 holds f . (A1 * A2) = (f . A1) * (f . A2)

hence
a . o is Homomorphism of G9,G9
by A7, GROUP_6:def 6; :: thesis: verumlet 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 A4, A8, FUNCT_1:1;

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 A4, A8, FUNCT_1:1;

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 A4, A8, FUNCT_1:1;

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: ( @ ((nat_hom H) . g1) = (nat_hom H) . g1 & @ ((nat_hom H) . g2) = (nat_hom H) . g2 ) ;

A26: ( (nat_hom H) . g1 = g1 * H & (nat_hom 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 A19, Lm8;

A28: A39 = g3 * H by A16, Lm8;

A29: B29 = h2 * H by A20, Lm8;

reconsider A19 = A19, A29 = A29, B19 = B19, B29 = B29 as Element of (G ./. H) ;

A2 = g2 * H by A12, A27, XTUPLE_0:1;

then A1 * A2 = the multF of G9 . (A19,A29) by A10, A27, XTUPLE_0:1

.= @ (A19 * A29) by A4, Def15

.= (@ A19) * (@ A29) by GROUP_6:20 ;

then A1 * A2 = (g1 * H) * (g2 * H) by A22, A27, Lm8

.= ((nat_hom H) . g1) * ((nat_hom H) . g2) by A25, A26, GROUP_6:19

.= (nat_hom H) . (g1 * g2) by GROUP_6:def 6

.= (g1 * g2) * H by GROUP_6:def 8 ;

then g3 * H = (g1 * g2) * H by A14, A28, XTUPLE_0:1;

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 A24, A21, A18, GROUP_6:32;

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 & (nat_hom H) . h2 = h2 * H ) by GROUP_6:def 8;

B39 = h3 * H by A17, Lm8;

then A32: f . (A1 * A2) = h3 * H by A14, XTUPLE_0:1;

A33: ( @ ((nat_hom H) . h1) = (nat_hom H) . h1 & @ ((nat_hom H) . h2) = (nat_hom H) . h2 ) ;

f . A2 = h2 * H by A12, A29, XTUPLE_0:1;

then (f . A1) * (f . A2) = the multF of G9 . (B19,B29) by A10, A29, XTUPLE_0:1

.= @ (B19 * B29) by A4, Def15

.= (@ B19) * (@ B29) by GROUP_6:20 ;

then (f . A1) * (f . A2) = (h1 * H) * (h2 * H) by A23, A29, Lm8

.= ((nat_hom H) . h1) * ((nat_hom H) . h2) by A33, A31, GROUP_6:19

.= (nat_hom H) . (h1 * h2) by GROUP_6:def 6

.= (h1 * h2) * H by GROUP_6:def 8 ;

hence f . (A1 * A2) = (f . A1) * (f . A2) by A32, A30, GROUP_2:114; :: thesis: verum

end;set A3 = A1 * A2;

set B1 = f . A1;

set B2 = f . A2;

set B3 = f . (A1 * A2);

[A1,(f . A1)] in f by A4, A8, FUNCT_1:1;

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 A4, A8, FUNCT_1:1;

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 A4, A8, FUNCT_1:1;

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: ( @ ((nat_hom H) . g1) = (nat_hom H) . g1 & @ ((nat_hom H) . g2) = (nat_hom H) . g2 ) ;

A26: ( (nat_hom H) . g1 = g1 * H & (nat_hom 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 A19, Lm8;

A28: A39 = g3 * H by A16, Lm8;

A29: B29 = h2 * H by A20, Lm8;

reconsider A19 = A19, A29 = A29, B19 = B19, B29 = B29 as Element of (G ./. H) ;

A2 = g2 * H by A12, A27, XTUPLE_0:1;

then A1 * A2 = the multF of G9 . (A19,A29) by A10, A27, XTUPLE_0:1

.= @ (A19 * A29) by A4, Def15

.= (@ A19) * (@ A29) by GROUP_6:20 ;

then A1 * A2 = (g1 * H) * (g2 * H) by A22, A27, Lm8

.= ((nat_hom H) . g1) * ((nat_hom H) . g2) by A25, A26, GROUP_6:19

.= (nat_hom H) . (g1 * g2) by GROUP_6:def 6

.= (g1 * g2) * H by GROUP_6:def 8 ;

then g3 * H = (g1 * g2) * H by A14, A28, XTUPLE_0:1;

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 A24, A21, A18, GROUP_6:32;

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 & (nat_hom H) . h2 = h2 * H ) by GROUP_6:def 8;

B39 = h3 * H by A17, Lm8;

then A32: f . (A1 * A2) = h3 * H by A14, XTUPLE_0:1;

A33: ( @ ((nat_hom H) . h1) = (nat_hom H) . h1 & @ ((nat_hom H) . h2) = (nat_hom H) . h2 ) ;

f . A2 = h2 * H by A12, A29, XTUPLE_0:1;

then (f . A1) * (f . A2) = the multF of G9 . (B19,B29) by A10, A29, XTUPLE_0:1

.= @ (B19 * B29) by A4, Def15

.= (@ B19) * (@ B29) by GROUP_6:20 ;

then (f . A1) * (f . A2) = (h1 * H) * (h2 * H) by A23, A29, Lm8

.= ((nat_hom H) . h1) * ((nat_hom H) . h2) by A33, A31, GROUP_6:19

.= (nat_hom H) . (h1 * h2) by GROUP_6:def 6

.= (h1 * h2) * H by GROUP_6:def 8 ;

hence f . (A1 * A2) = (f . A1) * (f . A2) by A32, A30, GROUP_2:114; :: thesis: verum

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)

hence
( G ./. N is distributive & G ./. N is Group-like & G ./. N is associative )
by A1, A2, GROUP_1:def 2, GROUP_1:def 3; :: thesis: verumlet 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 A34, GROUP_1:def 3; :: thesis: verum

end;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 A34, GROUP_1:def 3; :: thesis: verum