rng (Subst (t,x,p)) c= INT

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (Subst (t,x,p)) or y in INT )
assume A1: y in rng (Subst (t,x,p)) ; :: thesis: y in INT
consider b being object such that
A2: ( b in dom (Subst (t,x,p)) & (Subst (t,x,p)) . b = y ) by A1, FUNCT_1:def 3;
reconsider b = b as bag of O by A2;

per cases ( y = 0. F_Real or y <> 0. F_Real ) ;

suppose y = 0. F_Real ; :: thesis: y in INT

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

end;

suppose y <> 0. F_Real ; :: thesis: y in INT

then consider s being bag of O such that
A3: b = Subst (t,x,s) by A2, Def3;
y = (p `^ (t . x)) . s by Def3, A2, A3;
hence y in INT by INT_1:def 2; :: thesis: verum

end;

end;

end;

hence Subst (t,x,p) is INT -valued by RELAT_1:def 19; :: thesis: verum