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
A6: ( v = Sum l & rng l c= INT ) ;
reconsider a = i as Real by XREAL_0:def 1;
X1: a * l = i * l by LM000;
then reconsider f = i * l as Linear_Combination of A by RLVECT_2:67;
A7: i * v = Sum f by A6, X1, RLVECT_3:2;
rng (i * l) c= INT by LM002, A6;
hence i * v in Z_Lin A by A7; :: thesis: verum