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