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