theorem Th2: :: HFDIFF_1:2
for f1, f2 being PartFunc of REAL,REAL holds (- f1) (#) (- f2) = f1 (#) f2