let p be Element of REAL 3; :: thesis: |.p.| = sqrt ((((p . 1) ^2 ) + ((p . 2) ^2 )) + ((p . 3) ^2 ))
reconsider f = p as FinSequence of REAL ;
|.p.| = sqrt (Sum <*((p . 1) * (p . 1)),((p . 2) * (p . 2)),((p . 3) * (p . 3))*>) by Th36
.= sqrt ((((p . 1) ^2 ) + ((p . 2) ^2 )) + ((p . 3) ^2 )) by RVSUM_1:108 ;
hence |.p.| = sqrt ((((p . 1) ^2 ) + ((p . 2) ^2 )) + ((p . 3) ^2 )) ; :: thesis: verum