let x be real-valued FinSequence; :: thesis: |(x,x)| >= 0
set n = len x;
x is FinSequence of REAL by Lm2;
then reconsider w = x as Element of (len x) -tuples_on REAL by FINSEQ_2:92;
|(x,x)| = Sum (sqr w) ;
hence |(x,x)| >= 0 by Th86; :: thesis: verum