let f1, f2, f3 be complex-valued Function; :: thesis: f1 - (f2 - f3) = (f1 - f2) + f3
thus f1 - (f2 - f3) = (f1 - f2) - (- f3) by Tmp
.= (f1 - f2) + f3 ; :: thesis: verum