let C be non empty set ; :: thesis: for f, g being PartFunc of C,COMPLEX
for r being Complex holds r (#) (g / f) = (r (#) g) / f
let f, g be PartFunc of C,COMPLEX; :: 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 Th38
.= (r (#) g) (#) (f ^) by Th17
.= (r (#) g) / f by Th38 ; :: thesis: verum