let i be Integer; :: thesis: for V being RealLinearSpace
for A being Subset of V
for l being Linear_Combination of A st rng l c= INT holds
rng (i * l) c= INT
let V be RealLinearSpace; :: thesis: for A being Subset of V
for l being Linear_Combination of A st rng l c= INT holds
rng (i * l) c= INT
let A be Subset of V; :: thesis: for l being Linear_Combination of A st rng l c= INT holds
rng (i * l) c= INT
let l be Linear_Combination of A; :: thesis: ( rng l c= INT implies rng (i * l) c= INT )
assume AS: rng l c= INT ; :: thesis: rng (i * l) c= INT
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (i * l) or y in INT )
assume AD: y in rng (i * l) ; :: thesis: y in INT
consider x being set such that
R1: ( x in the carrier of V & y = (i * l) . x ) by AD, FUNCT_2:17;
reconsider z = x as VECTOR of V by R1;
reconsider ii = i as Real by XREAL_0:def 1;
l . z in rng l by FUNCT_2:6;
then reconsider z1 = l . z as Integer by AS;
(i * l) . z = (ii * l) . z by LM000
.= i * z1 by RLVECT_2:def 13 ;
hence y in INT by R1; :: thesis: verum