let V be ComplexLinearSpace; :: thesis: for M being non empty Subset of V holds 0c * M = {(0. V)}
let M be non empty Subset of V; :: thesis: 0c * M = {(0. V)}
for v being Element of V st v in {(0. V)} holds
v in 0c * M
proof
let v be Element of V; :: thesis: ( v in {(0. V)} implies v in 0c * M )
consider x being object such that
A1: x in M by XBOOLE_0:def 1;
reconsider x = x as Element of V by A1;
assume v in {(0. V)} ; :: thesis: v in 0c * M
then v = 0. V by TARSKI:def 1;
then v = 0c * x by CLVECT_1:1;
hence v in 0c * M by A1; :: thesis: verum
end;
then A2: {(0. V)} c= 0c * M ;
for v being Element of V st v in 0c * M holds
v in {(0. V)}
proof
let v be Element of V; :: thesis: ( v in 0c * M implies v in {(0. V)} )
assume v in 0c * M ; :: thesis: v in {(0. V)}
then ex x being Element of V st
( v = 0c * x & x in M ) ;
then v = 0. V by CLVECT_1:1;
hence v in {(0. V)} by TARSKI:def 1; :: thesis: verum
end;
then 0c * M c= {(0. V)} ;
hence 0c * M = {(0. V)} by A2, XBOOLE_0:def 10; :: thesis: verum