let H be non empty multMagma ; :: thesis: ( H is trivial implies ( H is Group-like & H is associative & H is commutative ) )
assume A1: H is trivial ; :: thesis: ( H is Group-like & H is associative & H is commutative )

hereby :: according to GROUP_1:def 3 :: thesis: ( H is associative & H is commutative )

consider e being Element of H;
take e = e; :: thesis: for h being Element of H holds
( h * e = h & e * h = h & ex g being Element of H st
( h * g = e & g * h = e ) )
let h be Element of H; :: thesis: ( h * e = h & e * h = h & ex g being Element of H st
( h * g = e & g * h = e ) )
thus ( h * e = h & e * h = h ) by A1, STRUCT_0:def 10; :: thesis: ex g being Element of H st
( h * g = e & g * h = e )
take g = e; :: thesis: ( h * g = e & g * h = e )
thus ( h * g = e & g * h = e ) by A1, STRUCT_0:def 10; :: thesis: verum

end;

thus for x, y, z being Element of H holds (x * y) * z = x * (y * z) by A1, STRUCT_0:def 10; :: according to GROUP_1:def 4 :: thesis: H is commutative
let x, y be Element of H; :: according to GROUP_1:def 16 :: thesis: x * y = y * x
thus x * y = y * x by A1, STRUCT_0:def 10; :: thesis: verum