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