let x, y, z be Element of 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 ) by FINSEQ_1:62;
hence |(p,p)| = ((x ^2 ) + (y ^2 )) + (z ^2 ) by Lm8; :: thesis: verum