let p, q be Element of REAL 3; :: thesis: for f1, f2, f3, g1, g2, g3 being PartFunc of ,
for t1, t2 being Real st p = (VFunc f1,f2,f3) . t1 & q = (VFunc g1,g2,g3) . t2 holds
p <X> q = |[(((f2 . t1) * (g3 . t2)) - ((f3 . t1) * (g2 . t2))),(((f3 . t1) * (g1 . t2)) - ((f1 . t1) * (g3 . t2))),(((f1 . t1) * (g2 . t2)) - ((f2 . t1) * (g1 . t2)))]|
let f1, f2, f3, g1, g2, g3 be PartFunc of ,; :: thesis: for t1, t2 being Real st p = (VFunc f1,f2,f3) . t1 & q = (VFunc g1,g2,g3) . t2 holds
p <X> q = |[(((f2 . t1) * (g3 . t2)) - ((f3 . t1) * (g2 . t2))),(((f3 . t1) * (g1 . t2)) - ((f1 . t1) * (g3 . t2))),(((f1 . t1) * (g2 . t2)) - ((f2 . t1) * (g1 . t2)))]|
let t1, t2 be Real; :: thesis: ( p = (VFunc f1,f2,f3) . t1 & q = (VFunc g1,g2,g3) . t2 implies p <X> q = |[(((f2 . t1) * (g3 . t2)) - ((f3 . t1) * (g2 . t2))),(((f3 . t1) * (g1 . t2)) - ((f1 . t1) * (g3 . t2))),(((f1 . t1) * (g2 . t2)) - ((f2 . t1) * (g1 . t2)))]| )
assume ( p = (VFunc f1,f2,f3) . t1 & q = (VFunc g1,g2,g3) . t2 ) ; :: thesis: p <X> q = |[(((f2 . t1) * (g3 . t2)) - ((f3 . t1) * (g2 . t2))),(((f3 . t1) * (g1 . t2)) - ((f1 . t1) * (g3 . t2))),(((f1 . t1) * (g2 . t2)) - ((f2 . t1) * (g1 . t2)))]|
then ( p = |[(f1 . t1),(f2 . t1),(f3 . t1)]| & q = |[(g1 . t2),(g2 . t2),(g3 . t2)]| ) by Def1;
hence p <X> q = |[(((f2 . t1) * (g3 . t2)) - ((f3 . t1) * (g2 . t2))),(((f3 . t1) * (g1 . t2)) - ((f1 . t1) * (g3 . t2))),(((f1 . t1) * (g2 . t2)) - ((f2 . t1) * (g1 . t2)))]| by Lm11; :: thesis: verum