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 )
assume A3: y in {0 } ; :: thesis: y in 0 ** A
consider t being set such that
A4: t in A by A1, XBOOLE_0:def 1;
reconsider t = t as Element of A by A4;
reconsider t = t as Real by A4;
y = 0 * t by A3, TARSKI:def 1;
hence y in 0 ** A by A4, 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 A5: y in 0 ** A ; :: thesis: y in {0 }
then reconsider y = y as Real ;
consider z being Real such that
A6: ( z in A & y = 0 * z ) by A5, INTEGRA2:def 2;
thus y in {0 } by A6, TARSKI:def 1; :: thesis: verum

end;

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