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

rng f c= INT by RELAT_1:def 19;

hence f is FinSequence of INT by FINSEQ_1:def 4; :: thesis: verum