let f be integer-yielding FinSequence; :: thesis: f is FinSequence of INT
rng f c= INT by VALUED_0:def 5;
hence f is FinSequence of INT by FINSEQ_1:def 4; :: thesis: verum