let O be set ; :: thesis: for G being strict Group ex H being non empty HGrWOpStr of 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 of 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 Lm2;
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 of O ;
reconsider G' = GO as non empty multMagma ;

A1: now

set e = 1_ G;
reconsider e' = 1_ G as Element of ;
take e' = e'; :: thesis: for h' being Element of holds
( h' * e' = h' & e' * h' = h' & ex g' being Element of st
( h' * g' = e' & g' * h' = e' ) )
let h' be Element of ; :: thesis: ( h' * e' = h' & e' * h' = h' & ex g' being Element of st
( h' * g' = e' & g' * h' = e' ) )
reconsider h = h' as Element of ;
set g = h " ;
reconsider g' = h " as Element of ;
h' * e' = h * (1_ G)
.= h by GROUP_1:def 5 ;
hence h' * e' = h' ; :: thesis: ( e' * h' = h' & ex g' being Element of st
( h' * g' = e' & g' * h' = e' ) )
e' * h' = (1_ G) * h
.= h by GROUP_1:def 5 ;
hence e' * h' = h' ; :: thesis: ex g' being Element of st
( h' * g' = e' & g' * h' = e' )
take g' = g'; :: thesis: ( h' * g' = e' & g' * h' = e' )
h' * g' = h * (h " )
.= 1_ G by GROUP_1:def 6 ;
hence h' * g' = e' ; :: thesis: g' * h' = e'
g' * h' = (h " ) * h
.= 1_ G by GROUP_1:def 6 ;
hence g' * h' = e' ; :: thesis: verum

end;

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

A2: now

let G'' be Group; :: thesis: for a being Action of O,the carrier of G'' st a = the action of GO & multMagma(# the carrier of G'',the multF of G'' #) = multMagma(# the carrier of GO,the multF of GO #) holds
a is distributive
let a be Action of O,the carrier of G''; :: thesis: ( a = the action of GO & multMagma(# the carrier of G'',the multF of G'' #) = 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 G'',the multF of G'' #) = multMagma(# the carrier of GO,the multF of GO #) implies a is distributive )
assume A4: multMagma(# the carrier of G'',the multF of G'' #) = multMagma(# the carrier of GO,the multF of GO #) ; :: thesis: a is distributive

now

let o be Element of O; :: thesis: ( o in O implies a . o is Homomorphism of G'',G'' )
assume o in O ; :: thesis: a . o is Homomorphism of G'',G''
then o in dom h by FUNCT_2:def 1;
then [o,(h . o)] in [:O,{(id the carrier of G'')}:] by A4, FUNCT_1:8;
then consider x, y being set such that
x in O and
A5: ( y in {(id the carrier of G'')} & [o,(h . o)] = [x,y] ) by ZFMISC_1:def 2;
( y = id the carrier of G'' & h . o = y ) by A5, TARSKI:def 1, ZFMISC_1:33;
hence a . o is Homomorphism of G'',G'' by A3, GROUP_6:47; :: thesis: verum

end;

hence a is distributive by Def4; :: thesis: verum

end;

now

let x', y', z' be Element of ; :: thesis: (x' * y') * z' = x' * (y' * z')
reconsider x = x', y = y', z = z' as Element of ;
(x' * y') * z' = (x * y) * z
.= x * (y * z) by GROUP_1:def 4 ;
hence (x' * y') * z' = x' * (y' * z') ; :: thesis: verum

end;

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