let p be Element of REAL 3; :: thesis: |.p.| = sqrt ((((p . 1) ^2) + ((p . 2) ^2)) + ((p . 3) ^2))
|.p.| = sqrt (Sum <*((p . 1) * (p . 1)),((p . 2) * (p . 2)),((p . 3) * (p . 3))*>) by Th43
.= sqrt ((((p . 1) ^2) + ((p . 2) ^2)) + ((p . 3) ^2)) by RVSUM_1:78 ;
hence |.p.| = sqrt ((((p . 1) ^2) + ((p . 2) ^2)) + ((p . 3) ^2)) ; :: thesis: verum