let f be integer-valued FinSequence; :: thesis: f is FinSequence of INT
thus rng f c= INT by VALUED_0:def 5; :: according to FINSEQ_1:def 4 :: thesis: verum