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 Th1;
hence |(p,p)| = (((p . 1) ^2) + ((p . 2) ^2)) + ((p . 3) ^2) by Lm12; :: thesis: verum