thus
rng (a * p) 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 (a * p) or y in INT )

assume A1: y in rng (a * p) ; :: thesis: y in INT

consider x being object such that

A2: ( x in dom (a * p) & (a * p) . x = y ) by A1, FUNCT_1:def 3;

reconsider x = x as bag of X by A2;

(a * p) . x = a * (p . x) by POLYNOM7:def 9;

hence y in INT by A2, INT_1:def 2; :: thesis: verum

end;assume A1: y in rng (a * p) ; :: thesis: y in INT

consider x being object such that

A2: ( x in dom (a * p) & (a * p) . x = y ) by A1, FUNCT_1:def 3;

reconsider x = x as bag of X by A2;

(a * p) . x = a * (p . x) by POLYNOM7:def 9;

hence y in INT by A2, INT_1:def 2; :: thesis: verum