(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