let x be real-valued FinSequence; :: thesis: 0 <= |.x.|
( |.x.| = sqrt |(x,x)| & 0 <= |(x,x)| ) by RVSUM_1:149, Th13;
hence 0 <= |.x.| by SQUARE_1:def 4; :: thesis: verum