theorem Th14: :: RFUNCT_1:14

for f1, f2, f3 being complex-valued Function holds (f1 - f2) (#) f3 = (f1 (#) f3) - (f2 (#) f3)