let p be Element of REAL 3; :: thesis: for f1, f2, f3 being PartFunc of ,
for t being Real st p = (VFunc f1,f2,f3) . t holds
|(p,(0.REAL 3))| = 0
let f1, f2, f3 be PartFunc of ,; :: thesis: for t being Real st p = (VFunc f1,f2,f3) . t holds
|(p,(0.REAL 3))| = 0
let t be Real; :: thesis: ( p = (VFunc f1,f2,f3) . t implies |(p,(0.REAL 3))| = 0 )
assume A0: p = (VFunc f1,f2,f3) . t ; :: thesis: |(p,(0.REAL 3))| = 0
A1: 0.REAL 3 = |[0 ,0 ,0 ]| by FINSEQ_2:76;
A2: (0.REAL 3) . 1 = 0 by A1, FINSEQ_1:62;
A3: (0.REAL 3) . 2 = 0 by A1, FINSEQ_1:62;
A4: (0.REAL 3) . 3 = 0 by A1, FINSEQ_1:62;
B0: p = |[(f1 . t),(f2 . t),(f3 . t)]| by A0, Def1;
B1: p . 1 = f1 . t by B0, FINSEQ_1:62;
B2: p . 2 = f2 . t by B0, FINSEQ_1:62;
B3: p . 3 = f3 . t by B0, FINSEQ_1:62;
|(p,(0.REAL 3))| = (((f1 . t) * 0 ) + ((f2 . t) * 0 )) + ((f3 . t) * 0 ) by A2, A3, A4, B1, B2, B3, Lm8;
hence |(p,(0.REAL 3))| = 0 ; :: thesis: verum