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