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

for v being Element of V st v in 0 * M holds

v in {(0. V)}

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

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

then A2:
{(0. V)} c= 0 * M
;
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;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

for v being Element of V st v in 0 * M holds

v in {(0. V)}

proof

then
0 * M c= {(0. V)}
;
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;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

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