let C be non empty set ; :: thesis: for f1, f2 being PartFunc of C,COMPLEX holds |.(f1 / f2).| = |.f1.| / |.f2.|
let f1, f2 be PartFunc of C,COMPLEX; :: thesis: |.(f1 / f2).| = |.f1.| / |.f2.|
thus |.(f1 / f2).| = |.(f1 (#) (f2 ^)).| by Th38
.= |.f1.| (#) |.(f2 ^).| by Th29
.= |.f1.| (#) (|.f2.| ^) by Th37
.= |.f1.| / |.f2.| by RFUNCT_1:31 ; :: thesis: verum