let x1, x2, x3, y1, y2, y3 be Element of REAL ; :: thesis: |[x1,x2,x3]| <X> |[y1,y2,y3]| = |[((x2 * y3) - (x3 * y2)),((x3 * y1) - (x1 * y3)),((x1 * y2) - (x2 * y1))]|
set p1 = |[x1,x2,x3]|;
A1: ( |[x1,x2,x3]| . 1 = x1 & |[x1,x2,x3]| . 2 = x2 & |[x1,x2,x3]| . 3 = x3 ) by FINSEQ_1:45;
set p2 = |[y1,y2,y3]|;
( |[y1,y2,y3]| . 1 = y1 & |[y1,y2,y3]| . 2 = y2 & |[y1,y2,y3]| . 3 = y3 ) by FINSEQ_1:45;
hence |[x1,x2,x3]| <X> |[y1,y2,y3]| = |[((x2 * y3) - (x3 * y2)),((x3 * y1) - (x1 * y3)),((x1 * y2) - (x2 * y1))]| by A1; :: thesis: verum