theorem :: RFUNCT_1:29

for f being complex-valued Function holds (- f) ^ = (- 1) (#) (f ^) by Lm1, Th28;