let f1, f2 be PartFunc of REAL , REAL ; :: thesis: (- f1) (#) (- f2) = f1 (#) f2
(- f1) (#) (- f2) = (- 1) (#) (f1 (#) (- f2)) by RFUNCT_1:24
.= f1 (#) (- (- f2)) by RFUNCT_1:25 ;
hence (- f1) (#) (- f2) = f1 (#) f2 ; :: thesis: verum