let x be FinSequence of REAL ; :: thesis: |.x.| ^2 = |(x,x)|
reconsider z = x as Element of (len x) -tuples_on REAL by FINSEQ_2:110;
A2: 0 <= |(x,x)| by Th11;
|.x.| ^2 = (sqrt (Sum (sqr x))) ^2 by EUCLID:def 5
.= |(x,x)| by A2, SQUARE_1:def 4 ;
hence |.x.| ^2 = |(x,x)| ; :: thesis: verum