let x1, x2, x3, y1, y2, y3 be Real; |[x1,x2,x3]| + |[y1,y2,y3]| = (((x1 + y1) * <e1>) + ((x2 + y2) * <e2>)) + ((x3 + y3) * <e3>)
A1:
( <e1> . 1 = 1 & <e1> . 2 = 0 & <e1> . 3 = 0 )
by FINSEQ_1:45;
A2:
( <e2> . 1 = 0 & <e2> . 2 = 1 & <e2> . 3 = 0 )
by FINSEQ_1:45;
A3:
( <e3> . 1 = 0 & <e3> . 2 = 0 & <e3> . 3 = 1 )
by FINSEQ_1:45;
A4: (((x1 + y1) * <e1>) + ((x2 + y2) * <e2>)) + ((x3 + y3) * <e3>) =
(|[((x1 + y1) * 1),((x1 + y1) * 0),((x1 + y1) * 0)]| + ((x2 + y2) * <e2>)) + ((x3 + y3) * <e3>)
by A1, Lm1
.=
(|[(x1 + y1),0,0]| + |[((x2 + y2) * 0),((x2 + y2) * 1),((x2 + y2) * 0)]|) + ((x3 + y3) * <e3>)
by A2, Lm1
.=
(|[(x1 + y1),0,0]| + |[0,(x2 + y2),0]|) + |[((x3 + y3) * 0),((x3 + y3) * 0),((x3 + y3) * 1)]|
by A3, Lm1
.=
(|[(x1 + y1),0,0]| + |[0,(x2 + y2),0]|) + |[0,0,(x3 + y3)]|
;
A5:
( |[(x1 + y1),0,0]| . 1 = x1 + y1 & |[(x1 + y1),0,0]| . 2 = 0 & |[(x1 + y1),0,0]| . 3 = 0 )
by FINSEQ_1:45;
A6:
( |[0,(x2 + y2),0]| . 1 = 0 & |[0,(x2 + y2),0]| . 2 = x2 + y2 & |[0,(x2 + y2),0]| . 3 = 0 )
by FINSEQ_1:45;
A7:
( |[0,0,(x3 + y3)]| . 1 = 0 & |[0,0,(x3 + y3)]| . 2 = 0 & |[0,0,(x3 + y3)]| . 3 = x3 + y3 )
by FINSEQ_1:45;
A8: (((x1 + y1) * <e1>) + ((x2 + y2) * <e2>)) + ((x3 + y3) * <e3>) =
|[((x1 + y1) + 0),(0 + (x2 + y2)),(0 + 0)]| + |[0,0,(x3 + y3)]|
by A4, A5, A6, Lm2
.=
|[(x1 + y1),(x2 + y2),0]| + |[0,0,(x3 + y3)]|
;
( |[(x1 + y1),(x2 + y2),0]| . 1 = x1 + y1 & |[(x1 + y1),(x2 + y2),0]| . 2 = x2 + y2 & |[(x1 + y1),(x2 + y2),0]| . 3 = 0 )
by FINSEQ_1:45;
then A9: (((x1 + y1) * <e1>) + ((x2 + y2) * <e2>)) + ((x3 + y3) * <e3>) =
|[((x1 + y1) + 0),((x2 + y2) + 0),(0 + (x3 + y3))]|
by A8, A7, Lm2
.=
|[(x1 + y1),(x2 + y2),(x3 + y3)]|
;
A10:
( |[x1,x2,x3]| . 1 = x1 & |[x1,x2,x3]| . 2 = x2 & |[x1,x2,x3]| . 3 = x3 )
by FINSEQ_1:45;
( |[y1,y2,y3]| . 1 = y1 & |[y1,y2,y3]| . 2 = y2 & |[y1,y2,y3]| . 3 = y3 )
by FINSEQ_1:45;
hence
|[x1,x2,x3]| + |[y1,y2,y3]| = (((x1 + y1) * <e1>) + ((x2 + y2) * <e2>)) + ((x3 + y3) * <e3>)
by A10, Lm2, A9; verum