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:91; :: thesis: verum

end;

assume p = 0.REAL 3 ; :: thesis: |(p,p)| = 0
then A1: p = |[0,0,0]| by FINSEQ_2:62;
then A2: p . 1 = 0 ;
A3: p . 2 = 0 by A1;
p . 3 = 0 by A1;
then |(p,p)| = ((0 ^2) + (0 ^2)) + (0 ^2) by A2, A3, Th55;
hence |(p,p)| = 0 ; :: thesis: verum