reconsider g = - f as INT -valued Function ;
(1 / 2) (#) ((abs g) + g) is natural-valued ;
then (1 / 2) (#) ((abs g) - f) is natural-valued by VALUED_1:def 9;
hence (1 / 2) (#) ((abs f) - f) is natural-valued by EUCLID:5; :: thesis: verum