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 A1: |.p.| = 0 ; :: thesis: p = 0.REAL 3
|(p,p)| >= 0 by RVSUM_1:119;
then (sqrt |(p,p)|) ^2 = |(p,p)| by SQUARE_1:def 2;
hence p = 0.REAL 3 by A1, Th79; :: thesis: verum

end;

assume p = 0.REAL 3 ; :: thesis: |.p.| = 0
then A2: p = |[0,0,0]| by FINSEQ_2:62;
then A3: p . 1 = 0 by FINSEQ_1:45;
A4: p . 2 = 0 by A2, FINSEQ_1:45;
p . 3 = 0 by A2, FINSEQ_1:45;
then |(p,p)| = ((0 ^2) + (0 ^2)) + (0 ^2) by A3, A4, Th64;
hence |.p.| = 0 by SQUARE_1:17; :: thesis: verum