theorem Th24: :: RFUNCT_1:24

for f1, f2 being complex-valued Function holds abs (f1 (#) f2) = (abs f1) (#) (abs f2)