let C be non empty set ; :: thesis: for g, f being PartFunc of C,COMPLEX
for r being Element of COMPLEX holds r (#) (g / f) = (r (#) g) / f
let g, f be PartFunc of C,COMPLEX ; :: thesis: for r being Element of COMPLEX holds r (#) (g / f) = (r (#) g) / f
let r be Element of COMPLEX ; :: thesis: r (#) (g / f) = (r (#) g) / f
thus r (#) (g / f) = r (#) (g (#) (f ^ )) by Th51
.= (r (#) g) (#) (f ^ ) by Th26
.= (r (#) g) / f by Th51 ; :: thesis: verum