let H be 1 -element multMagma ; :: thesis: ( H is Group-like & H is associative & H is commutative )

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

set e = the Element of H;
take e = the Element of H; :: 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 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 STRUCT_0:def 10; :: thesis: verum

end;

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