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