theorem Th2: :: EUCLID:5

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