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 A1: rng l c= INT ; :: thesis: rng (i * l) c= INT
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (i * l) or y in INT )
assume A2: y in rng (i * l) ; :: thesis: y in INT
consider x being object such that
A3: ( x in the carrier of V & y = (i * l) . x ) by A2, FUNCT_2:11;
reconsider z = x as VECTOR of V by A3;
reconsider ii = i as Real ;
l . z in rng l by FUNCT_2:4;
then reconsider z1 = l . z as Integer by A1;
(i * l) . z = (ii * l) . z by Th4
.= i * z1 by RLVECT_2:def 11 ;
hence y in INT by A3, INT_1:def 2; :: thesis: verum