(- 1) (#) f1 is empty-yielding dom f -defined total Function ;
then reconsider f2 = - f1 as empty-yielding dom f -defined total Function by VALUED_1:def 6;
f + f2 = f ;
hence f - f1 = f by VALUED_1:def 9; :: thesis: verum