let f1, f2 be complex-valued Function; :: thesis: (f1 / f2) ^ = (f2 | (dom (f2 ^))) / f1
thus (f1 / f2) ^ = (f1 (#) (f2 ^)) ^ by Th31
.= (f1 ^) (#) ((f2 ^) ^) by Th27
.= (f2 | (dom (f2 ^))) (#) (f1 ^) by Th26
.= (f2 | (dom (f2 ^))) / f1 by Th31 ; :: thesis: verum