theorem :: TOPREAL7:11

for f, g being FinSequence of REAL holds abs (f ^ g) = (abs f) ^ (abs g)