let x be real-valued FinSequence; :: thesis: |.x.| = sqrt |(x,x)|
|.x.| = sqrt (|.x.| ^2) by EUCLID:9, SQUARE_1:22
.= sqrt |(x,x)| by Th4 ;
hence |.x.| = sqrt |(x,x)| ; :: thesis: verum