let f1, f2 be complex-valued Function; :: thesis: abs (f1 / f2) = (abs f1) / (abs f2)
thus abs (f1 / f2) = abs (f1 (#) (f2 ^)) by Th31
.= (abs f1) (#) (abs (f2 ^)) by Th24
.= (abs f1) (#) ((abs f2) ^) by Th30
.= (abs f1) / (abs f2) by Th31 ; :: thesis: verum