let V be RealLinearSpace; :: thesis: for v being VECTOR of V
for a being Real
for W being Subspace of V st v in W holds
a * v in W
let v be VECTOR of V; :: thesis: for a being Real
for W being Subspace of V st v in W holds
a * v in W
let a be Real; :: thesis: for W being Subspace of V st v in W holds
a * v in W
let W be Subspace of V; :: thesis: ( v in W implies a * v in W )
reconsider VW = the carrier of W as Subset of V by Def2;
assume v in W ; :: thesis: a * v in W
then A1: v in the carrier of W ;
VW is linearly-closed by Lm1;
then a * v in the carrier of W by A1;
hence a * v in W ; :: thesis: verum