let f be real-valued FinSequence; :: thesis: |.f.| ^2 = Sum (sqr f)
Sum (sqr f) >= 0 by RVSUM_1:116;
hence |.f.| ^2 = Sum (sqr f) by SQUARE_1:def 4; :: thesis: verum