let G be non empty Group-like multMagma ; :: thesis: for A being Subset of G holds
( (1_ G) * A = A & A * (1_ G) = A )
let A be Subset of G; :: thesis: ( (1_ G) * A = A & A * (1_ G) = A )
thus (1_ G) * A = A :: thesis: A * (1_ G) = A

proof

thus (1_ G) * A c= A :: according to XBOOLE_0:def 10 :: thesis: A c= (1_ G) * A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (1_ G) * A or x in A )
assume x in (1_ G) * A ; :: thesis: x in A
then ex h being Element of G st
( x = (1_ G) * h & h in A ) by Th27;
hence x in A by GROUP_1:def 4; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in (1_ G) * A )
assume A1: x in A ; :: thesis: x in (1_ G) * A
then reconsider a = x as Element of G ;
(1_ G) * a = a by GROUP_1:def 4;
hence x in (1_ G) * A by A1, Th27; :: thesis: verum

end;

thus A * (1_ G) c= A :: according to XBOOLE_0:def 10 :: thesis: A c= A * (1_ G)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A * (1_ G) or x in A )
assume x in A * (1_ G) ; :: thesis: x in A
then ex h being Element of G st
( x = h * (1_ G) & h in A ) by Th28;
hence x in A by GROUP_1:def 4; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in A * (1_ G) )
assume A2: x in A ; :: thesis: x in A * (1_ G)
then reconsider a = x as Element of G ;
a * (1_ G) = a by GROUP_1:def 4;
hence x in A * (1_ G) by A2, Th28; :: thesis: verum