let x, y, z be Real; :: thesis: for p being Element of REAL 3 st p = |[x,y,z]| holds
|(p,p)| = ((x ^2) + (y ^2)) + (z ^2)
let p be Element of REAL 3; :: thesis: ( p = |[x,y,z]| implies |(p,p)| = ((x ^2) + (y ^2)) + (z ^2) )
assume p = |[x,y,z]| ; :: thesis: |(p,p)| = ((x ^2) + (y ^2)) + (z ^2)
then ( p . 1 = x & p . 2 = y & p . 3 = z ) ;
hence |(p,p)| = ((x ^2) + (y ^2)) + (z ^2) by Lm5; :: thesis: verum