let V be RealLinearSpace; :: thesis: for M being non empty Subset of V holds 0 * M = {(0. V)}
let M be non empty Subset of V; :: thesis: 0 * M = {(0. V)}
for v being Element of V st v in {(0. V)} holds
v in 0 * M

proof

let v be Element of V; :: thesis: ( v in {(0. V)} implies v in 0 * 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 0 * M
then v = 0. V by TARSKI:def 1;
then v = 0 * x by RLVECT_1:10;
hence v in 0 * M by A1; :: thesis: verum

end;

then A2: {(0. V)} c= 0 * M ;
for v being Element of V st v in 0 * M holds
v in {(0. V)}

proof

let v be Element of V; :: thesis: ( v in 0 * M implies v in {(0. V)} )
assume v in 0 * M ; :: thesis: v in {(0. V)}
then ex x being Element of V st
( v = 0 * x & x in M ) ;
then v = 0. V by RLVECT_1:10;
hence v in {(0. V)} by TARSKI:def 1; :: thesis: verum

end;

then 0 * M c= {(0. V)} ;
hence 0 * M = {(0. V)} by A2; :: thesis: verum