rng (f mod m) c= INT by RELAT_1:def 19;
hence f mod m is FinSequence of INT by FINSEQ_1:def 4; :: thesis: verum