set g = f mod m;
let y be object ; :: according to VALUED_0:def 11 :: thesis: ( not y in dom (f mod m) or (f mod m) . y is integer )
assume A1: y in dom (f mod m) ; :: thesis: (f mod m) . y is integer
dom (f mod m) = dom f by Def1;
then (f mod m) . y = (f . y) mod m by A1, Def1;
hence (f mod m) . y is integer ; :: thesis: verum