let V be RealLinearSpace; :: thesis: for A being Subset of V
for l1, l2 being Linear_Combination of A st rng l1 c= INT & rng l2 c= INT holds
rng (l1 + l2) c= INT
let A be Subset of V; :: thesis: for l1, l2 being Linear_Combination of A st rng l1 c= INT & rng l2 c= INT holds
rng (l1 + l2) c= INT
let l1, l2 be Linear_Combination of A; :: thesis: ( rng l1 c= INT & rng l2 c= INT implies rng (l1 + l2) c= INT )
assume A1: ( rng l1 c= INT & rng l2 c= INT ) ; :: thesis: rng (l1 + l2) c= INT
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (l1 + l2) or y in INT )
assume A2: y in rng (l1 + l2) ; :: thesis: y in INT
consider x being object such that
A3: ( x in the carrier of V & y = (l1 + l2) . x ) by A2, FUNCT_2:11;
reconsider z = x as VECTOR of V by A3;
l1 . z in rng l1 by FUNCT_2:4;
then reconsider z1 = l1 . z as Integer by A1;
l2 . z in rng l2 by FUNCT_2:4;
then reconsider z2 = l2 . z as Integer by A1;
(l1 + l2) . z = z1 + z2 by RLVECT_2:def 10;
hence y in INT by A3, INT_1:def 2; :: thesis: verum