let x be real-valued FinSequence; :: thesis: |.x.| ^2 = |(x,x)|

A1: 0 <= |(x,x)| by RVSUM_1:119;

|.x.| ^2 = (sqrt (Sum (sqr x))) ^2 by EUCLID:def 5

.= |(x,x)| by A1, SQUARE_1:def 2 ;

hence |.x.| ^2 = |(x,x)| ; :: thesis: verum

A1: 0 <= |(x,x)| by RVSUM_1:119;

|.x.| ^2 = (sqrt (Sum (sqr x))) ^2 by EUCLID:def 5

.= |(x,x)| by A1, SQUARE_1:def 2 ;

hence |.x.| ^2 = |(x,x)| ; :: thesis: verum