let O be set ; :: thesis:
let G be strict Group; :: thesis:
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 over O ;
reconsider G9 = GO as non empty multMagma ;

A1: now :: thesis:

set e = 1_ G;
reconsider e9 = 1_ G as Element of G9 ;
take e9 = e9; :: thesis:
let h9 be Element of G9; :: thesis:
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 = (1_ G) * h
.= h by GROUP_1:def 4 ;
hence e9 * h9 = h9 ; :: thesis:
take g9 = g9; :: thesis:
h9 * g9 = h * (h ")
.= 1_ G by GROUP_1:def 5 ;
hence h9 * g9 = e9 ; :: thesis:
g9 * h9 = (h ") * h
.= 1_ G by GROUP_1:def 5 ;
hence g9 * h9 = e9 ; :: thesis:

end;

take GO ; :: thesis:

A2: now :: thesis:

let G99 be Group; :: thesis:
let a be Action of O, the carrier of G99; :: thesis:
assume A3: a = the action of GO ; :: thesis:
assume A4: multMagma(# the carrier of G99, the multF of G99 #) = multMagma(# the carrier of GO, the multF of GO #) ; :: thesis:

now :: thesis:

let o be Element of O; :: thesis:
assume o in O ; :: thesis:
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 set 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:

end;

hence a is distributive by Def4; :: thesis:

end;

now :: thesis:

let x9, y9, z9 be Element of G9; :: thesis:
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:

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 2, GROUP_1:def 3; :: thesis: