let x, y, z be Element of REAL ; |[x,y,z]| = ((x * <e1> ) + (y * <e2> )) + (z * <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;
set p = |[x,y,z]|;
A6: ((x * <e1> ) + (y * <e2> )) + (z * <e3> ) =
(|[(x * 1),(x * 0 ),(x * 0 )]| + (y * <e2> )) + (z * <e3> )
by A2, Lm3
.=
(|[x,0 ,0 ]| + |[(y * 0 ),(y * 1),(y * 0 )]|) + (z * <e3> )
by A3, Lm3
.=
(|[x,0 ,0 ]| + |[0 ,y,0 ]|) + |[(z * 0 ),(z * 0 ),(z * 1)]|
by A4, Lm3
.=
(|[x,0 ,0 ]| + |[0 ,y,0 ]|) + |[0 ,0 ,z]|
;
A7:
( |[x,0 ,0 ]| . 1 = x & |[x,0 ,0 ]| . 2 = 0 & |[x,0 ,0 ]| . 3 = 0 )
by FINSEQ_1:62;
A8:
( |[0 ,y,0 ]| . 1 = 0 & |[0 ,y,0 ]| . 2 = y & |[0 ,y,0 ]| . 3 = 0 )
by FINSEQ_1:62;
A9:
( |[0 ,0 ,z]| . 1 = 0 & |[0 ,0 ,z]| . 2 = 0 & |[0 ,0 ,z]| . 3 = z )
by FINSEQ_1:62;
A10: ((x * <e1> ) + (y * <e2> )) + (z * <e3> ) =
|[(x + 0 ),(y + 0 ),(0 + 0 )]| + |[0 ,0 ,z]|
by A6, A7, A8, Lm4
.=
|[x,y,0 ]| + |[0 ,0 ,z]|
;
A11:
( |[x,y,0 ]| . 1 = x & |[x,y,0 ]| . 2 = y & |[x,y,0 ]| . 3 = 0 )
by FINSEQ_1:62;
((x * <e1> ) + (y * <e2> )) + (z * <e3> ) =
|[(x + 0 ),(y + 0 ),(0 + z)]|
by A9, A10, A11, Lm4
.=
|[x,y,z]|
;
hence
|[x,y,z]| = ((x * <e1> ) + (y * <e2> )) + (z * <e3> )
; verum