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