let i be Integer; :: thesis: for V being RealLinearSpace
for v being VECTOR of V
for A being Subset of V st v in Z_Lin A holds
i * v in Z_Lin A
let V be RealLinearSpace; :: thesis: for v being VECTOR of V
for A being Subset of V st v in Z_Lin A holds
i * v in Z_Lin A
let v be VECTOR of V; :: thesis: for A being Subset of V st v in Z_Lin A holds
i * v in Z_Lin A
let A be Subset of V; :: thesis: ( v in Z_Lin A implies i * v in Z_Lin A )
assume v in Z_Lin A ; :: thesis: i * v in Z_Lin A
then consider l being Linear_Combination of A such that
A1: ( v = Sum l & rng l c= INT ) ;
reconsider a = i as Real ;
A2: a * l = i * l by Th4;
then reconsider f = i * l as Linear_Combination of A by RLVECT_2:44;
A3: i * v = Sum f by A1, A2, RLVECT_3:2;
rng (i * l) c= INT by Th6, A1;
hence i * v in Z_Lin A by A3; :: thesis: verum