let V be ComplexLinearSpace; :: thesis: for v being VECTOR of V
for z being Complex
for W being Subspace of V st v in W holds
z * v in W
let v be VECTOR of V; :: thesis: for z being Complex
for W being Subspace of V st v in W holds
z * v in W
let z be Complex; :: thesis: for W being Subspace of V st v in W holds
z * v in W
let W be Subspace of V; :: thesis: ( v in W implies z * v in W )
reconsider VW = the carrier of W as Subset of V by Def8;
assume v in W ; :: thesis: z * v in W
then A1: v in the carrier of W by STRUCT_0:def 5;
VW is linearly-closed by Lm3;
then z * v in the carrier of W by A1, Def7;
hence z * v in W by STRUCT_0:def 5; :: thesis: verum