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