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