let A be non empty ext-real-membered set ; :: thesis: 0 ** A = {0}
for e being object holds
( e in 0 ** A iff e = 0 )

proof

let e be object ; :: thesis: ( e in 0 ** A iff e = 0 )
consider r being ExtReal such that
A1: r in A by MEMBERED:8;

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

assume e in 0 ** A ; :: thesis: e = 0
then ex z being Element of ExtREAL st
( e = 0 * z & z in A ) by MEMBER_1:188;
hence e = 0 ; :: thesis: verum

end;

assume e = 0 ; :: thesis: e in 0 ** A
then e = 0 * r ;
hence e in 0 ** A by A1, MEMBER_1:186; :: thesis: verum

end;

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