let x1, x2, x3, y1, y2, y3 be Element of REAL ; |[x1,x2,x3]| + |[y1,y2,y3]| = (((x1 + y1) * <e1> ) + ((x2 + y2) * <e2> )) + ((x3 + y3) * <e3> )
A2:
( <e1> . 1 = 1 & <e1> . 2 = 0 & <e1> . 3 = 0 )
by FINSEQ_1:62;
A3:
( <e2> . 1 = 0 & <e2> . 2 = 1 & <e2> . 3 = 0 )
by FINSEQ_1:62;
A4:
( <e3> . 1 = 0 & <e3> . 2 = 0 & <e3> . 3 = 1 )
by FINSEQ_1:62;
A1: (((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 A2, Lm3
.=
(|[(x1 + y1),0 ,0 ]| + |[((x2 + y2) * 0 ),((x2 + y2) * 1),((x2 + y2) * 0 )]|) + ((x3 + y3) * <e3> )
by A3, Lm3
.=
(|[(x1 + y1),0 ,0 ]| + |[0 ,(x2 + y2),0 ]|) + |[((x3 + y3) * 0 ),((x3 + y3) * 0 ),((x3 + y3) * 1)]|
by A4, Lm3
.=
(|[(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:62;
A6:
( |[0 ,(x2 + y2),0 ]| . 1 = 0 & |[0 ,(x2 + y2),0 ]| . 2 = x2 + y2 & |[0 ,(x2 + y2),0 ]| . 3 = 0 )
by FINSEQ_1:62;
A7:
( |[0 ,0 ,(x3 + y3)]| . 1 = 0 & |[0 ,0 ,(x3 + y3)]| . 2 = 0 & |[0 ,0 ,(x3 + y3)]| . 3 = x3 + y3 )
by FINSEQ_1:62;
A0: (((x1 + y1) * <e1> ) + ((x2 + y2) * <e2> )) + ((x3 + y3) * <e3> ) =
|[((x1 + y1) + 0 ),(0 + (x2 + y2)),(0 + 0 )]| + |[0 ,0 ,(x3 + y3)]|
by A1, A5, A6, Lm4
.=
|[(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:62;
then A9: (((x1 + y1) * <e1> ) + ((x2 + y2) * <e2> )) + ((x3 + y3) * <e3> ) =
|[((x1 + y1) + 0 ),((x2 + y2) + 0 ),(0 + (x3 + y3))]|
by A0, A7, Lm4
.=
|[(x1 + y1),(x2 + y2),(x3 + y3)]|
;
B1:
( |[x1,x2,x3]| . 1 = x1 & |[x1,x2,x3]| . 2 = x2 & |[x1,x2,x3]| . 3 = x3 )
by FINSEQ_1:62;
( |[y1,y2,y3]| . 1 = y1 & |[y1,y2,y3]| . 2 = y2 & |[y1,y2,y3]| . 3 = y3 )
by FINSEQ_1:62;
hence
|[x1,x2,x3]| + |[y1,y2,y3]| = (((x1 + y1) * <e1> ) + ((x2 + y2) * <e2> )) + ((x3 + y3) * <e3> )
by B1, Lm4, A9; verum