let O be set ; :: thesis: for G being strict Group ex H being non empty HGrWOpStr over O st

( H is strict & H is distributive & H is Group-like & H is associative & G = multMagma(# the carrier of H, the multF of H #) )

let G be strict Group; :: thesis: ex H being non empty HGrWOpStr over O st

( H is strict & H is distributive & H is Group-like & H is associative & G = multMagma(# the carrier of H, the multF of H #) )

reconsider h = [:O,{(id the carrier of G)}:] as Action of O, the carrier of G by Lm1;

set A = the carrier of G;

set m = the multF of G;

set GO = HGrWOpStr(# the carrier of G, the multF of G,h #);

reconsider GO = HGrWOpStr(# the carrier of G, the multF of G,h #) as non empty HGrWOpStr over O ;

reconsider G9 = GO as non empty multMagma ;

( H is strict & H is distributive & H is Group-like & H is associative & G = multMagma(# the carrier of H, the multF of H #) )

let G be strict Group; :: thesis: ex H being non empty HGrWOpStr over O st

( H is strict & H is distributive & H is Group-like & H is associative & G = multMagma(# the carrier of H, the multF of H #) )

reconsider h = [:O,{(id the carrier of G)}:] as Action of O, the carrier of G by Lm1;

set A = the carrier of G;

set m = the multF of G;

set GO = HGrWOpStr(# the carrier of G, the multF of G,h #);

reconsider GO = HGrWOpStr(# the carrier of G, the multF of G,h #) as non empty HGrWOpStr over O ;

reconsider G9 = GO as non empty multMagma ;

A1: now :: thesis: ex e9 being Element of G9 st

for h9 being Element of G9 holds

( h9 * e9 = h9 & e9 * h9 = h9 & ex g9 being Element of G9 st

( h9 * g9 = e9 & g9 * h9 = e9 ) )

take
GO
; :: thesis: ( GO is strict & GO is distributive & GO is Group-like & GO is associative & G = multMagma(# the carrier of GO, the multF of GO #) )for h9 being Element of G9 holds

( h9 * e9 = h9 & e9 * h9 = h9 & ex g9 being Element of G9 st

( h9 * g9 = e9 & g9 * h9 = e9 ) )

set e = 1_ G;

reconsider e9 = 1_ G as Element of G9 ;

take e9 = e9; :: thesis: for h9 being Element of G9 holds

( h9 * e9 = h9 & e9 * h9 = h9 & ex g9 being Element of G9 st

( h9 * g9 = e9 & g9 * h9 = e9 ) )

let h9 be Element of G9; :: thesis: ( h9 * e9 = h9 & e9 * h9 = h9 & ex g9 being Element of G9 st

( h9 * g9 = e9 & g9 * h9 = e9 ) )

reconsider h = h9 as Element of G ;

set g = h " ;

reconsider g9 = h " as Element of G9 ;

h9 * e9 = h * (1_ G)

.= h by GROUP_1:def 4 ;

hence h9 * e9 = h9 ; :: thesis: ( e9 * h9 = h9 & ex g9 being Element of G9 st

( h9 * g9 = e9 & g9 * h9 = e9 ) )

e9 * h9 = (1_ G) * h

.= h by GROUP_1:def 4 ;

hence e9 * h9 = h9 ; :: thesis: ex g9 being Element of G9 st

( h9 * g9 = e9 & g9 * h9 = e9 )

take g9 = g9; :: thesis: ( h9 * g9 = e9 & g9 * h9 = e9 )

h9 * g9 = h * (h ")

.= 1_ G by GROUP_1:def 5 ;

hence h9 * g9 = e9 ; :: thesis: g9 * h9 = e9

g9 * h9 = (h ") * h

.= 1_ G by GROUP_1:def 5 ;

hence g9 * h9 = e9 ; :: thesis: verum

end;reconsider e9 = 1_ G as Element of G9 ;

take e9 = e9; :: thesis: for h9 being Element of G9 holds

( h9 * e9 = h9 & e9 * h9 = h9 & ex g9 being Element of G9 st

( h9 * g9 = e9 & g9 * h9 = e9 ) )

let h9 be Element of G9; :: thesis: ( h9 * e9 = h9 & e9 * h9 = h9 & ex g9 being Element of G9 st

( h9 * g9 = e9 & g9 * h9 = e9 ) )

reconsider h = h9 as Element of G ;

set g = h " ;

reconsider g9 = h " as Element of G9 ;

h9 * e9 = h * (1_ G)

.= h by GROUP_1:def 4 ;

hence h9 * e9 = h9 ; :: thesis: ( e9 * h9 = h9 & ex g9 being Element of G9 st

( h9 * g9 = e9 & g9 * h9 = e9 ) )

e9 * h9 = (1_ G) * h

.= h by GROUP_1:def 4 ;

hence e9 * h9 = h9 ; :: thesis: ex g9 being Element of G9 st

( h9 * g9 = e9 & g9 * h9 = e9 )

take g9 = g9; :: thesis: ( h9 * g9 = e9 & g9 * h9 = e9 )

h9 * g9 = h * (h ")

.= 1_ G by GROUP_1:def 5 ;

hence h9 * g9 = e9 ; :: thesis: g9 * h9 = e9

g9 * h9 = (h ") * h

.= 1_ G by GROUP_1:def 5 ;

hence g9 * h9 = e9 ; :: thesis: verum

A2: now :: thesis: for G99 being Group

for a being Action of O, the carrier of G99 st a = the action of GO & multMagma(# the carrier of G99, the multF of G99 #) = multMagma(# the carrier of GO, the multF of GO #) holds

a is distributive

for a being Action of O, the carrier of G99 st a = the action of GO & multMagma(# the carrier of G99, the multF of G99 #) = multMagma(# the carrier of GO, the multF of GO #) holds

a is distributive

let G99 be Group; :: thesis: for a being Action of O, the carrier of G99 st a = the action of GO & multMagma(# the carrier of G99, the multF of G99 #) = multMagma(# the carrier of GO, the multF of GO #) holds

a is distributive

let a be Action of O, the carrier of G99; :: thesis: ( a = the action of GO & multMagma(# the carrier of G99, the multF of G99 #) = multMagma(# the carrier of GO, the multF of GO #) implies a is distributive )

assume A3: a = the action of GO ; :: thesis: ( multMagma(# the carrier of G99, the multF of G99 #) = multMagma(# the carrier of GO, the multF of GO #) implies a is distributive )

assume A4: multMagma(# the carrier of G99, the multF of G99 #) = multMagma(# the carrier of GO, the multF of GO #) ; :: thesis: a is distributive

end;a is distributive

let a be Action of O, the carrier of G99; :: thesis: ( a = the action of GO & multMagma(# the carrier of G99, the multF of G99 #) = multMagma(# the carrier of GO, the multF of GO #) implies a is distributive )

assume A3: a = the action of GO ; :: thesis: ( multMagma(# the carrier of G99, the multF of G99 #) = multMagma(# the carrier of GO, the multF of GO #) implies a is distributive )

assume A4: multMagma(# the carrier of G99, the multF of G99 #) = multMagma(# the carrier of GO, the multF of GO #) ; :: thesis: a is distributive

now :: thesis: for o being Element of O st o in O holds

a . o is Homomorphism of G99,G99

hence
a is distributive
; :: thesis: veruma . o is Homomorphism of G99,G99

let o be Element of O; :: thesis: ( o in O implies a . o is Homomorphism of G99,G99 )

assume o in O ; :: thesis: a . o is Homomorphism of G99,G99

then o in dom h by FUNCT_2:def 1;

then [o,(h . o)] in [:O,{(id the carrier of G99)}:] by A4, FUNCT_1:1;

then consider x, y being object such that

x in O and

A5: ( y in {(id the carrier of G99)} & [o,(h . o)] = [x,y] ) by ZFMISC_1:def 2;

( y = id the carrier of G99 & h . o = y ) by A5, TARSKI:def 1, XTUPLE_0:1;

hence a . o is Homomorphism of G99,G99 by A3, GROUP_6:38; :: thesis: verum

end;assume o in O ; :: thesis: a . o is Homomorphism of G99,G99

then o in dom h by FUNCT_2:def 1;

then [o,(h . o)] in [:O,{(id the carrier of G99)}:] by A4, FUNCT_1:1;

then consider x, y being object such that

x in O and

A5: ( y in {(id the carrier of G99)} & [o,(h . o)] = [x,y] ) by ZFMISC_1:def 2;

( y = id the carrier of G99 & h . o = y ) by A5, TARSKI:def 1, XTUPLE_0:1;

hence a . o is Homomorphism of G99,G99 by A3, GROUP_6:38; :: thesis: verum

now :: thesis: for x9, y9, z9 being Element of G9 holds (x9 * y9) * z9 = x9 * (y9 * z9)

hence
( GO is strict & GO is distributive & GO is Group-like & GO is associative & G = multMagma(# the carrier of GO, the multF of GO #) )
by A1, A2, GROUP_1:def 2, GROUP_1:def 3; :: thesis: verumlet x9, y9, z9 be Element of G9; :: thesis: (x9 * y9) * z9 = x9 * (y9 * z9)

reconsider x = x9, y = y9, z = z9 as Element of G ;

(x9 * y9) * z9 = (x * y) * z

.= x * (y * z) by GROUP_1:def 3 ;

hence (x9 * y9) * z9 = x9 * (y9 * z9) ; :: thesis: verum

end;reconsider x = x9, y = y9, z = z9 as Element of G ;

(x9 * y9) * z9 = (x * y) * z

.= x * (y * z) by GROUP_1:def 3 ;

hence (x9 * y9) * z9 = x9 * (y9 * z9) ; :: thesis: verum