set f = ALiouville_seq (a,b);
rng (ALiouville_seq (a,b)) c= INT

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (ALiouville_seq (a,b)) or y in INT )
assume y in rng (ALiouville_seq (a,b)) ; :: thesis: y in INT
then consider x being object such that
A1: ( x in dom (ALiouville_seq (a,b)) & y = (ALiouville_seq (a,b)) . x ) by FUNCT_1:def 3;
reconsider x = x as Nat by A1;
y is Integer by Th29, A1;
hence y in INT by INT_1:def 2; :: thesis: verum

end;

hence ALiouville_seq (a,b) is INT -valued by RELAT_1:def 19; :: thesis: verum