theorem Th10: :: RFUNCT_1:10

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