theorem :: CFUNCT_1:33
for f1, f2 being complex-valued Function holds f1 - (- f2) = f1 + f2 ;