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