let x1, y1, z1, x2, y2, z2 be Real; :: thesis: |[x1,y1,z1]| + |[x2,y2,z2]| = |[(x1 + x2),(y1 + y2),(z1 + z2)]|
A4: |[x2,y2,z2]| . 1 = x2 by FINSEQ_1:62;
A5: |[x2,y2,z2]| . 2 = y2 by FINSEQ_1:62;
A6: |[x2,y2,z2]| . 3 = z2 by FINSEQ_1:62;
A7: (|[x1,y1,z1]| . 1) + (|[x2,y2,z2]| . 1) = x1 + x2 by A4, FINSEQ_1:62;
A8: (|[x1,y1,z1]| . 2) + (|[x2,y2,z2]| . 2) = y1 + y2 by A5, FINSEQ_1:62;
(|[x1,y1,z1]| . 3) + (|[x2,y2,z2]| . 3) = z1 + z2 by A6, FINSEQ_1:62;
hence |[x1,y1,z1]| + |[x2,y2,z2]| = |[(x1 + x2),(y1 + y2),(z1 + z2)]| by A7, A8, EUCLID_8:55; :: thesis: verum