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