let G be non empty addGroup-like addMagma ; :: thesis: for A being Subset of G holds
( (0_ G) + A = A & A + (0_ G) = A )
let A be Subset of G; :: thesis: ( (0_ G) + A = A & A + (0_ G) = A )
thus (0_ G) + A = A :: thesis: A + (0_ G) = A
proof
thus (0_ G) + A c= A :: according to XBOOLE_0:def 10 :: thesis: A c= (0_ G) + A
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (0_ G) + A or x in A )
assume x in (0_ G) + A ; :: thesis: x in A
then ex h being Element of G st
( x = (0_ G) + h & h in A ) by Th27;
hence x in A by Def4; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in (0_ G) + A )
assume A1: x in A ; :: thesis: x in (0_ G) + A
then reconsider a = x as Element of G ;
(0_ G) + a = a by Def4;
hence x in (0_ G) + A by A1, Th27; :: thesis: verum
end;
thus A + (0_ G) c= A :: according to XBOOLE_0:def 10 :: thesis: A c= A + (0_ G)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A + (0_ G) or x in A )
assume x in A + (0_ G) ; :: thesis: x in A
then ex h being Element of G st
( x = h + (0_ G) & h in A ) by Th28;
hence x in A by Def4; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in A + (0_ G) )
assume A2: x in A ; :: thesis: x in A + (0_ G)
then reconsider a = x as Element of G ;
a + (0_ G) = a by Def4;
hence x in A + (0_ G) by A2, Th28; :: thesis: verum