let A be non empty Subset of REAL ; :: thesis: 0 ** A = {0 }
for e being set holds
( e in 0 ** A iff e = 0 )

proof

let e be set ; :: thesis: ( e in 0 ** A iff e = 0 )

hereby :: thesis: ( e = 0 implies e in 0 ** A )

assume Z: e in 0 ** A ; :: thesis: e = 0
ex z being Real st
( z in A & e = 0 * z ) by Z, Def2;
hence e = 0 ; :: thesis: verum

end;

consider r being real number such that
W: r in A by MEMBERED:9;
assume e = 0 ; :: thesis: e in 0 ** A
then e = 0 * r ;
hence e in 0 ** A by W, Def2; :: thesis: verum

end;

hence 0 ** A = {0 } by TARSKI:def 1; :: thesis: verum