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

hereby :: thesis: ( f is Integer_Sequence implies f is sequence of INT )

assume f is sequence of INT ; :: thesis: f is Integer_Sequence
then reconsider g = f as sequence of INT ;
( dom g = NAT & ( for x being object 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 sequence of INT
then ( dom f = NAT & rng f c= INT ) by FUNCT_2:def 1, RELAT_1:def 19;
hence f is sequence of INT by FUNCT_2:2; :: thesis: verum