let f1, f2, f3 be PartFunc of ,; :: thesis: for t being Real
for p being Element of REAL 3 st p = (VFunc f1,f2,f3) . t holds
( |.p.| = 0 iff p = 0.REAL 3 )
let t be Real; :: thesis: for p being Element of REAL 3 st p = (VFunc f1,f2,f3) . t holds
( |.p.| = 0 iff p = 0.REAL 3 )
let p be Element of REAL 3; :: thesis: ( p = (VFunc f1,f2,f3) . t implies ( |.p.| = 0 iff p = 0.REAL 3 ) )
assume A1: p = (VFunc f1,f2,f3) . t ; :: 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 A1, 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;
A8: p = |[(f1 . t),(f2 . t),(f3 . t)]| by A1, Def1;
A12: f1 . t = 0 by A8, FINSEQ_1:62, A5;
A13: f2 . t = 0 by A8, FINSEQ_1:62, A6;
A14: f3 . t = 0 by A8, FINSEQ_1:62, A7;
|(p,p)| = ((0 ^2 ) + (0 ^2 )) + (0 ^2 ) by A12, A13, A14, A1, Th52;
hence |.p.| = 0 by SQUARE_1:82; :: thesis: verum