let x1, x2, y1, y2, z1, z2 be Real; |[x1,y1,z1]| <X> |[x2,y2,z2]| = |[((y1 * z2) - (z1 * y2)),((z1 * x2) - (x1 * z2)),((x1 * y2) - (y1 * x2))]|
consider p1 being Point of (TOP-REAL 3) such that
A1:
p1 = |[x1,y1,z1]|
;
A2:
p1 `3 = z1
by A1, FINSEQ_1:45;
consider p2 being Point of (TOP-REAL 3) such that
A3:
p2 = |[x2,y2,z2]|
;
A4:
p2 `3 = z2
by A3, FINSEQ_1:45;
A5:
( p2 `1 = x2 & p2 `2 = y2 )
by A3, FINSEQ_1:45;
( p1 `1 = x1 & p1 `2 = y1 )
by A1, FINSEQ_1:45;
hence
|[x1,y1,z1]| <X> |[x2,y2,z2]| = |[((y1 * z2) - (z1 * y2)),((z1 * x2) - (x1 * z2)),((x1 * y2) - (y1 * x2))]|
by A1, A2, A3, A5, A4; verum