let A be complex-membered set ; :: thesis: ( A <> {} implies 0 ** A = {0} )
assume A1: A <> {} ; :: thesis: 0 ** A = {0}
A2: {0} c= 0 ** A
proof
set x = the Element of A;
let a be Nat; :: according to MEMBERED:def 12 :: thesis: ( not a in {0} or a in 0 ** A )
assume A3: a in {0} ; :: thesis: a in 0 ** A
A4: 0 * the Element of A in { (0 * c) where c is Complex : c in A } by A1;
0 ** A = { (0 * c) where c is Complex : c in A } by Th194;
hence a in 0 ** A by A3, A4, TARSKI:def 1; :: thesis: verum
end;
0 ** A c= {0} by Th201;
hence 0 ** A = {0} by A2; :: thesis: verum