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