let p1, p2 be Element of REAL 3; :: thesis: for f1, f2, f3 being PartFunc of ,
for t1, t2 being Real st p1 = (VFunc f1,f2,f3) . t1 & p2 = (VFunc f1,f2,f3) . t2 holds
|{p2,p1,p2}| = 0
let f1, f2, f3 be PartFunc of ,; :: thesis: for t1, t2 being Real st p1 = (VFunc f1,f2,f3) . t1 & p2 = (VFunc f1,f2,f3) . t2 holds
|{p2,p1,p2}| = 0
let t1, t2 be Real; :: thesis: ( p1 = (VFunc f1,f2,f3) . t1 & p2 = (VFunc f1,f2,f3) . t2 implies |{p2,p1,p2}| = 0 )
assume A1: ( p1 = (VFunc f1,f2,f3) . t1 & p2 = (VFunc f1,f2,f3) . t2 ) ; :: thesis: |{p2,p1,p2}| = 0
A2: p2 = |[(f1 . t2),(f2 . t2),(f3 . t2)]| by A1, Def1;
A3: p2 . 1 = f1 . t2 by A2, FINSEQ_1:62;
A4: p2 . 2 = f2 . t2 by A2, FINSEQ_1:62;
A5: p2 . 3 = f3 . t2 by A2, FINSEQ_1:62;
A6: p1 <X> p2 = |[(((f2 . t1) * (f3 . t2)) - ((f3 . t1) * (f2 . t2))),(((f3 . t1) * (f1 . t2)) - ((f1 . t1) * (f3 . t2))),(((f1 . t1) * (f2 . t2)) - ((f2 . t1) * (f1 . t2)))]| by A1, Th55;
A7: (p1 <X> p2) . 1 = ((f2 . t1) * (f3 . t2)) - ((f3 . t1) * (f2 . t2)) by A6, FINSEQ_1:62;
A8: (p1 <X> p2) . 2 = ((f3 . t1) * (f1 . t2)) - ((f1 . t1) * (f3 . t2)) by A6, FINSEQ_1:62;
A9: (p1 <X> p2) . 3 = ((f1 . t1) * (f2 . t2)) - ((f2 . t1) * (f1 . t2)) by A6, FINSEQ_1:62;
|{p2,p1,p2}| = (((f1 . t2) * (((f2 . t1) * (f3 . t2)) - ((f3 . t1) * (f2 . t2)))) + ((f2 . t2) * (((f3 . t1) * (f1 . t2)) - ((f1 . t1) * (f3 . t2))))) + ((f3 . t2) * (((f1 . t1) * (f2 . t2)) - ((f2 . t1) * (f1 . t2)))) by A9, A8, A7, A3, A4, A5, Lm8
.= 0 ;
hence |{p2,p1,p2}| = 0 ; :: thesis: verum