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 Th51
.= |.f1.| (#) |.(f2 ^ ).| by Th38
.= |.f1.| (#) (|.f2.| ^ ) by Th50
.= |.f1.| / |.f2.| by RFUNCT_1:47 ; :: thesis: verum