thus rng (p + q) c= INT :: according to RELAT_1:def 19 :: thesis: verum

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (p + q) or y in INT )
assume A3: y in rng (p + q) ; :: thesis: y in INT
consider x being object such that
A4: ( x in dom (p + q) & (p + q) . x = y ) by A3, FUNCT_1:def 3;
reconsider x = x as bag of X by A4;
(p + q) . x = (p . x) + (q . x) by POLYNOM1:15;
hence y in INT by A4, INT_1:def 2; :: thesis: verum

end;