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