let H be 1 -element multMagma ; :: thesis: ( H is Group-like & H is associative & 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

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

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 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;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

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