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