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