let x be FinSequence of REAL ; :: thesis: |.x.| = sqrt |(x,x)|
|.x.| = sqrt (|.x.| ^2 ) by EUCLID:12, SQUARE_1:89
.= sqrt |(x,x)| by Th12 ;
hence |.x.| = sqrt |(x,x)| ; :: thesis: verum