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