let M be strict multMagma ; :: thesis: ( ex x being object st the carrier of M = {x} implies ex G being trivial strict Group st M = G )
given x being object such that A1: the carrier of M = {x} ; :: thesis: ex G being trivial strict Group st M = G
reconsider M = M as non empty multMagma by A1;
reconsider x = x as Element of M by A1, TARSKI:def 1;
A2: for a, b, c being Element of M holds (a * b) * c = a * (b * c)

proof

let a, b, c be Element of M; :: thesis: (a * b) * c = a * (b * c)
( (a * b) * c = x & a * (b * c) = x ) by A1, TARSKI:def 1;
hence (a * b) * c = a * (b * c) ; :: thesis: verum

end;

ex e being Element of M st
for h being Element of M holds
( h * e = h & e * h = h & ex g being Element of M st
( h * g = e & g * h = e ) )

proof

take e = x; :: thesis: for h being Element of M holds
( h * e = h & e * h = h & ex g being Element of M st
( h * g = e & g * h = e ) )
let h be Element of M; :: thesis: ( h * e = h & e * h = h & ex g being Element of M st
( h * g = e & g * h = e ) )
h = x by A1, TARSKI:def 1;
hence ( h * e = h & e * h = h ) by A1, TARSKI:def 1; :: thesis: ex g being Element of M st
( h * g = e & g * h = e )
take g = x; :: thesis: ( h * g = e & g * h = e )
thus ( h * g = e & g * h = e ) by A1, TARSKI:def 1; :: thesis: verum

end;

then reconsider G = M as trivial strict Group by A1, A2, GROUP_1:def 2, GROUP_1:def 3;
take G ; :: thesis: M = G
thus M = G ; :: thesis: verum