theorem Th4: :: MATRTOP1:4

for rf being real-valued FinSequence holds sqrt (rf ^2) = abs rf