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 )

for e being object holds

( e in 0 ** A iff e = 0 )

proof

hence
0 ** A = {0}
by TARSKI:def 1; :: thesis: verum
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;

then e = 0 * r ;

hence e in 0 ** A by A1, MEMBER_1:186; :: thesis: verum

end;consider r being ExtReal such that

A1: r in A by MEMBERED:8;

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

assume
e = 0
; :: thesis: e in 0 ** Aassume
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;then ex z being Element of ExtREAL st

( e = 0 * z & z in A ) by MEMBER_1:188;

hence e = 0 ; :: thesis: verum

then e = 0 * r ;

hence e in 0 ** A by A1, MEMBER_1:186; :: thesis: verum