let p be Element of REAL 3; :: thesis: |(p,p)| = (((p . 1) ^2 ) + ((p . 2) ^2 )) + ((p . 3) ^2 )
p = |[(p . 1),(p . 2),(p . 3)]| by Lm1;
hence |(p,p)| = (((p . 1) ^2 ) + ((p . 2) ^2 )) + ((p . 3) ^2 ) by LmTh8; :: thesis: verum