let g, f be complex-valued Function; :: thesis: for r being complex number holds r (#) (g / f) = (r (#) g) / f
let r be complex number ; :: thesis: r (#) (g / f) = (r (#) g) / f
thus r (#) (g / f) = r (#) (g (#) (f ^ )) by Th47
.= (r (#) g) (#) (f ^ ) by Th24
.= (r (#) g) / f by Th47 ; :: thesis: verum