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