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]|
;
( |[x,y,0]| . 1 = x & |[x,y,0]| . 2 = y & |[x,y,0]| . 3 = 0 )
by FINSEQ_1:62;
then ((x * <e1>) + (y * <e2>)) + (z * <e3>) =
|[(x + 0),(y + 0),(0 + z)]|
by A9, A10, Lm4
.=
|[x,y,z]|
;
hence
|[x,y,z]| = ((x * <e1>) + (y * <e2>)) + (z * <e3>)
; verum