let A be Subset of REAL ; :: thesis: ( A <> {} implies 0 ** A = {0 } )
assume A1: A <> {} ; :: thesis: 0 ** A = {0 }
A2: {0 } c= 0 ** A

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in {0 } or y in 0 ** A )
consider t being set such that
A3: t in A by A1, XBOOLE_0:def 1;
reconsider t = t as Element of A by A3;
reconsider t = t as Real by A3;
assume y in {0 } ; :: thesis: y in 0 ** A
then y = 0 * t by TARSKI:def 1;
hence y in 0 ** A by A3, INTEGRA2:def 2; :: thesis: verum

end;

0 ** A c= {0 }

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in 0 ** A or y in {0 } )
assume A4: y in 0 ** A ; :: thesis: y in {0 }
then reconsider y = y as Real ;
ex z being Real st
( z in A & y = 0 * z ) by A4, INTEGRA2:def 2;
hence y in {0 } by TARSKI:def 1; :: thesis: verum

end;

hence 0 ** A = {0 } by A2, XBOOLE_0:def 10; :: thesis: verum