let x be FinSequence of REAL ; :: thesis: 0 <= |.x.|
A1: |.x.| = sqrt |(x,x)| by Th13;
0 <= |(x,x)| by Th11;
hence 0 <= |.x.| by A1, SQUARE_1:def 4; :: thesis: verum