let f be Function; :: thesis: ( f is Integer_Sequence iff ( dom f = NAT & ( for x being set st x in NAT holds
f . x is integer ) ) )
thus ( f is Integer_Sequence implies ( dom f = NAT & ( for x being set st x in NAT holds
f . x is integer ) ) ) by SEQ_1:3; :: thesis: ( dom f = NAT & ( for x being set st x in NAT holds
f . x is integer ) implies f is Integer_Sequence )
assume that
A1: dom f = NAT and
A2: for x being set st x in NAT holds
f . x is integer ; :: thesis: f is Integer_Sequence

now

let y be set ; :: thesis: ( y in rng f implies y in INT )
assume y in rng f ; :: thesis: y in INT
then consider x being set such that
A3: x in dom f and
A4: y = f . x by FUNCT_1:def 5;
f . x is integer by A1, A2, A3;
hence y in INT by A4, INT_1:def 2; :: thesis: verum

end;

then A5: rng f c= INT by TARSKI:def 3;
for x being set st x in NAT holds
f . x is real

proof

let x be set ; :: thesis: ( x in NAT implies f . x is real )
assume x in NAT ; :: thesis: f . x is real
then f . x is integer by A2;
hence f . x is real ; :: thesis: verum

end;

hence f is Integer_Sequence by A1, A5, SEQ_1:3, VALUED_0:def 5; :: thesis: verum