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,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,p)| = 0 iff p = 0.REAL 3 )
let p be Element of REAL 3; :: thesis: ( p = (VFunc f1,f2,f3) . t implies ( |(p,p)| = 0 iff p = 0.REAL 3 ) )
assume A1: p = (VFunc f1,f2,f3) . t ; :: 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 A2: |(p,p)| = 0 ; :: thesis: p = 0.REAL 3
Sum (sqr p) = 0 by A2;
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;
A8: p = |[(f1 . t),(f2 . t),(f3 . t)]| by A1, Def1;
A5: p . 1 = f1 . t by A8, FINSEQ_1:62;
A6: p . 2 = f2 . t by A8, FINSEQ_1:62;
A7: p . 3 = f3 . t by A8, FINSEQ_1:62;
A9: f1 . t = 0 by A4, FINSEQ_1:62, A5;
A10: f2 . t = 0 by A4, FINSEQ_1:62, A6;
A11: f3 . t = 0 by A4, FINSEQ_1:62, A7;
|(p,p)| = ((0 ^2 ) + (0 ^2 )) + (0 ^2 ) by A1, A9, A10, A11, Th52;
hence |(p,p)| = 0 ; :: thesis: verum