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