let x1, x2, x3, y1, y2, y3 be Real; :: thesis: |[x1,x2,x3]| + |[y1,y2,y3]| = |[(x1 + y1),(x2 + y2),(x3 + y3)]|
A4: (|[x1,x2,x3]| . 1) + (|[y1,y2,y3]| . 1) = x1 + y1 ;
A5: (|[x1,x2,x3]| . 2) + (|[y1,y2,y3]| . 2) = x2 + y2 ;
(|[x1,x2,x3]| . 3) + (|[y1,y2,y3]| . 3) = x3 + y3 ;
hence |[x1,x2,x3]| + |[y1,y2,y3]| = |[(x1 + y1),(x2 + y2),(x3 + y3)]| by A4, A5, Lm2; :: thesis: verum