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