let g, f1, f2 be complex-valued Function; :: thesis: g (#) (f1 / f2) = (g (#) f1) / f2
thus g (#) (f1 / f2) = g (#) (f1 (#) (f2 ^)) by Th47
.= (g (#) f1) (#) (f2 ^) by Th21
.= (g (#) f1) / f2 by Th47 ; :: thesis: verum