reconsider F = (1 / 2) (#) (f + (abs f)) as real-valued Function ;
for i being object holds F . i is natural

proof

let i be object ; :: thesis: F . i is natural

per cases ( i in dom F or not i in dom F ) ;

suppose B0: i in dom F ; :: thesis: F . i is natural

then B1: i in dom (f + (abs f)) by VALUED_1:def 5;
then B2: i in (dom f) /\ (dom (abs f)) by VALUED_1:def 1;
reconsider a = f . i as Integer ;
reconsider b = (abs f) . i as Nat ;
b = |.a.| by VALUED_1:def 11, B2;
then ( b = a or b = - a ) by ABSVALUE:1;
then ( a + b = b + b or a + b = (- b) + b ) ;
then ( (f + (abs f)) . i = 2 * b or (f + (abs f)) . i = 0 ) by B1, VALUED_1:def 1;
then ( F . i = (1 / 2) * (2 * b) or F . i = (1 / 2) * 0 ) by B0, VALUED_1:def 5;
hence F . i is natural ; :: thesis: verum

end;

suppose not i in dom F ; :: thesis: F . i is natural

hence F . i is natural by FUNCT_1:def 2; :: thesis: verum

end;

end;

end;

hence (1 / 2) (#) (f + (abs f)) is natural-valued by VALUED_0:12; :: thesis: verum