set f = ALiouville_seq (a,b);

rng (ALiouville_seq (a,b)) c= INT

rng (ALiouville_seq (a,b)) c= INT

proof

hence
ALiouville_seq (a,b) is INT -valued
by RELAT_1:def 19; :: thesis: verum
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;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