let p be Element of REAL 3; :: thesis: ( |(p,p)| = 0 iff p = 0.REAL 3 )
thus ( |(p,p)| = 0 implies p = 0.REAL 3 ) :: thesis: ( p = 0.REAL 3 implies |(p,p)| = 0 )

proof

assume |(p,p)| = 0 ; :: thesis: p = 0.REAL 3
then Sum (sqr p) = 0 ;
hence p = 0.REAL 3 by RVSUM_1:121; :: thesis: verum

end;

assume p = 0.REAL 3 ; :: thesis: |(p,p)| = 0
then A4: p = |[0 ,0 ,0 ]| by FINSEQ_2:76;
A9: p . 1 = 0 by A4, FINSEQ_1:62;
A10: p . 2 = 0 by A4, FINSEQ_1:62;
p . 3 = 0 by A4, FINSEQ_1:62;
then |(p,p)| = ((0 ^2 ) + (0 ^2 )) + (0 ^2 ) by A9, A10, Th52;
hence |(p,p)| = 0 ; :: thesis: verum