let f be Function; :: thesis: ( f is Function of NAT ,INT iff f is Integer_Sequence )

hereby :: thesis: ( f is Integer_Sequence implies f is Function of NAT ,INT )

assume f is Function of NAT ,INT ; :: thesis: f is Integer_Sequence
then reconsider g = f as Function of NAT ,INT ;
A1: dom g = NAT by FUNCT_2:def 1;
for x being set st x in NAT holds
g . x is integer ;
hence f is Integer_Sequence by A1, Th8; :: thesis: verum

end;

assume f is Integer_Sequence ; :: thesis: f is Function of NAT ,INT
then ( dom f = NAT & rng f c= INT ) by FUNCT_2:def 1, VALUED_0:def 5;
hence f is Function of NAT ,INT by FUNCT_2:4; :: thesis: verum