let x be real-valued FinSequence; :: thesis: |.x.| ^2 = |(x,x)|
x is FinSequence of REAL by Lm1;
then reconsider z = x as Element of (len x) -tuples_on REAL by FINSEQ_2:110;
A1: 0 <= |(x,x)| by RVSUM_1:149;
|.x.| ^2 = (sqrt (Sum (sqr x))) ^2 by EUCLID:def 5
.= |(x,x)| by A1, SQUARE_1:def 4 ;
hence |.x.| ^2 = |(x,x)| ; :: thesis: verum