let x be FinSequence of REAL ; :: thesis: |(x,x)| >= 0
reconsider z = x as Element of REAL (len x) by JORDAN2C:52;
set n = len x;
reconsider w = z as Element of (len x) -tuples_on REAL by EUCLID:def 1;
|(x,x)| = Sum (sqr w) ;
hence |(x,x)| >= 0 by RVSUM_1:116; :: thesis: verum