theorem Th30: :: RFUNCT_1:30

for f being complex-valued Function holds (abs f) ^ = abs (f ^)