f - 0 = (- 0) + f by VALUED_1:def 3;
hence f - 0 = f ; :: thesis: verum