let f be INT -valued FinSequence; :: thesis: f is FinSequence of INT
rng f c= INT by RELAT_1:def 19;
hence f is FinSequence of INT by FINSEQ_1:def 4; :: thesis: verum