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