let V be RealLinearSpace; :: thesis: for A being Subset of V holds 0 * A c= {(0. V)}

let A be Subset of V; :: thesis: 0 * A c= {(0. V)}

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in 0 * A or x in {(0. V)} )

assume x in 0 * A ; :: thesis: x in {(0. V)}

then ex v being Element of V st

( x = 0 * v & v in A ) ;

then x = 0. V by RLVECT_1:10;

hence x in {(0. V)} by TARSKI:def 1; :: thesis: verum

let A be Subset of V; :: thesis: 0 * A c= {(0. V)}

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in 0 * A or x in {(0. V)} )

assume x in 0 * A ; :: thesis: x in {(0. V)}

then ex v being Element of V st

( x = 0 * v & v in A ) ;

then x = 0. V by RLVECT_1:10;

hence x in {(0. V)} by TARSKI:def 1; :: thesis: verum