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 ;
( dom g = NAT & ( for x being set st x in NAT holds
g . x is integer ) ) by FUNCT_2:def 1;
hence f is Integer_Sequence by 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