theorem :: RFUNCT_1:43
for f1, f2 being complex-valued Function holds abs (f1 / f2) = (abs f1) / (abs f2)