theorem Th3: :: TOPREAL9:5

for f being real-valued FinSequence holds |.f.| ^2 = Sum (sqr f)