let x1, x2, x3, y1, y2, y3 be Real; |[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; verum