let f1, f2, f3 be complex-valued Function; :: thesis: (f1 - f2) (#) f3 = (f1 (#) f3) - (f2 (#) f3)
(- f2) (#) f3 = - (f2 (#) f3) by Th17;
hence (f1 - f2) (#) f3 = (f1 (#) f3) - (f2 (#) f3) by Th15; :: thesis: verum