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 A1: y in rng (p *' q) ; :: thesis: y in INT
consider x being object such that
A2: ( x in dom (p *' q) & (p *' q) . x = y ) by A1, FUNCT_1:def 3;
reconsider x = x as bag of X by A2;
consider s being FinSequence of F_Real such that
A3: ( (p *' q) . x = Sum s & len s = len (decomp x) ) and
A4: for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of X st
( (decomp x) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) by POLYNOM1:def 10;
consider f being sequence of F_Real such that
A5: ( Sum s = f . (len s) & f . 0 = 0. F_Real ) and
A6: for j being Nat
for v being Element of F_Real st j < len s & v = s . (j + 1) holds
f . (j + 1) = (f . j) + v by RLVECT_1:def 12;
defpred S₁[ Nat] means ( X <= len s implies f . X is integer );
A7: S₁[ 0 ] by A5;
A8: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A9: S₁[n] ; :: thesis: S₁[n + 1]
set n1 = n + 1;
assume A10: n + 1 <= len s ; :: thesis: f . (n + 1) is integer
A11: n + 1 in dom s by A10, FINSEQ_3:25, NAT_1:11;
then consider b1, b2 being bag of X such that
A12: ( (decomp x) /. (n + 1) = <*b1,b2*> & s /. (n + 1) = (p . b1) * (q . b2) ) by A4;
A13: s /. (n + 1) = s . (n + 1) by A11, PARTFUN1:def 6;
( f . n is integer & f . (n + 1) = (f . n) + (s /. (n + 1)) ) by A9, A6, A13, A10, NAT_1:13;
hence f . (n + 1) is integer by A12; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A7, A8);
then Sum s is integer by A5;
hence y in INT by A3, A2, INT_1:def 2; :: thesis: verum

end;