let O be set ; :: thesis:
let G be GroupWithOperators of O; :: thesis:
reconsider G9 = HGrWOpStr(# the carrier of G, the multF of G, the action of G #) as non empty multMagma ;

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;

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;

then reconsider G9 = G9 as non empty Group-like associative strict HGrWOpStr over O by A1, GROUP_1:def 2, GROUP_1:def 3;
for G being Group
for a being Action of O, the carrier of G st a = the action of G9 & multMagma(# the carrier of G, the multF of G #) = multMagma(# the carrier of G9, the multF of G9 #) holds
a is distributive by Def5;
then reconsider G9 = G9 as non empty Group-like associative distributive HGrWOpStr over O by Def5;

let o be Element of O; :: thesis:

then G9 ^ o = the action of G9 . o by Def6;
hence G9 ^ o = G ^ o by A4, Def6; :: thesis:

end;

end;

thus G9 ^ o = (G ^ o) | the carrier of G9 by A3; :: thesis:

end;