let x1, x2, x3, y1, y2, y3 be Real; |[x1,x2,x3]| - |[y1,y2,y3]| = |[(x1 - y1),(x2 - y2),(x3 - y3)]|
A1:
|[y1,y2,y3]| . 1 = y1
by FINSEQ_1:45;
A2:
|[y1,y2,y3]| . 2 = y2
by FINSEQ_1:45;
A3:
|[y1,y2,y3]| . 3 = y3
by FINSEQ_1:45;
A4:
(|[x1,x2,x3]| . 1) - (|[y1,y2,y3]| . 1) = x1 - y1
by A1, FINSEQ_1:45;
A5:
(|[x1,x2,x3]| . 2) - (|[y1,y2,y3]| . 2) = x2 - y2
by A2, FINSEQ_1:45;
(|[x1,x2,x3]| . 3) - (|[y1,y2,y3]| . 3) = x3 - y3
by A3, FINSEQ_1:45;
hence
|[x1,x2,x3]| - |[y1,y2,y3]| = |[(x1 - y1),(x2 - y2),(x3 - y3)]|
by A4, A5, Lm7; verum