let C be non empty set ; :: thesis: for f1, f2, g being PartFunc of C,COMPLEX holds g (#) (f1 / f2) = (g (#) f1) / f2
let f1, f2, g be PartFunc of C,COMPLEX; :: thesis: g (#) (f1 / f2) = (g (#) f1) / f2
thus g (#) (f1 / f2) = g (#) (f1 (#) (f2 ^)) by Th38
.= (g (#) f1) (#) (f2 ^) by Th14
.= (g (#) f1) / f2 by Th38 ; :: thesis: verum