let c1, c2 be Complex; :: thesis: for f, g being complex-valued Function holds (c1 (#) f) (#) (c2 (#) g) = (c1 * c2) (#) (f (#) g)
let f, g be complex-valued Function; :: thesis: (c1 (#) f) (#) (c2 (#) g) = (c1 * c2) (#) (f (#) g)
A1: (c2 * c1) (#) f = c2 (#) (c1 (#) f) by CFUNCT_1:22;
thus (c1 * c2) (#) (f (#) g) = ((c1 * c2) (#) f) (#) g by CFUNCT_1:17
.= c2 (#) ((c1 (#) f) (#) g) by A1, CFUNCT_1:17
.= (c1 (#) f) (#) (c2 (#) g) by CFUNCT_1:17 ; :: thesis: verum