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

proof

assume A2: |.p.| = 0 ; :: thesis: p = 0.REAL 3
A3: |(p,p)| >= 0 by RVSUM_1:149;
(sqrt |(p,p)|) ^2 = |(p,p)| by A3, SQUARE_1:def 4;
hence p = 0.REAL 3 by A2, ThA41; :: thesis: verum

end;

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