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

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

( (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
A * (1_ G) c= A
:: according to XBOOLE_0:def 10 :: thesis: A c= A * (1_ G)
thus
(1_ G) * A c= A
:: according to XBOOLE_0:def 10 :: thesis: A c= (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;proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in (1_ G) * A )
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;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

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in A * (1_ G) )
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;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

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