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 A5: y in rng (p - q) ; :: thesis: y in INT
consider x being object such that
A6: ( x in dom (p - q) & (p - q) . x = y ) by A5, FUNCT_1:def 3;
reconsider x = x as bag of X by A6;
p - q = p + (- q) by POLYNOM1:def 7;
then (p - q) . x = (p . x) + ((- q) . x) by POLYNOM1:15
.= (p . x) + (- (q . x)) by POLYNOM1:17 ;
hence y in INT by A6, INT_1:def 2; :: thesis: verum

end;