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