let G be addGroup; :: thesis: for A being Subset of G st A <> {} holds
(0_ G) * A = {(0_ G)}
let A be Subset of G; :: thesis: ( A <> {} implies (0_ G) * A = {(0_ G)} )
set y = the Element of A;
assume A1: A <> {} ; :: thesis: (0_ G) * A = {(0_ G)}
then reconsider y = the Element of A as Element of G by TARSKI:def 3;
thus (0_ G) * A c= {(0_ G)} :: according to XBOOLE_0:def 10 :: thesis: {(0_ G)} c= (0_ G) * A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (0_ G) * A or x in {(0_ G)} )
assume x in (0_ G) * A ; :: thesis: x in {(0_ G)}
then ex a being Element of G st
( x = (0_ G) * a & a in A ) by ThB42;
then x = 0_ G by Th17;
hence x in {(0_ G)} by TARSKI:def 1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(0_ G)} or x in (0_ G) * A )
assume x in {(0_ G)} ; :: thesis: x in (0_ G) * A
then x = 0_ G by TARSKI:def 1;
then (0_ G) * y = x by Th17;
hence x in (0_ G) * A by A1, ThB42; :: thesis: verum