let p1, p2 be Element of REAL 3; p1 + p2 = ((((p1 . 1) + (p2 . 1)) * <e1> ) + (((p1 . 2) + (p2 . 2)) * <e2> )) + (((p1 . 3) + (p2 . 3)) * <e3> )
A1:
( <e1> . 1 = 1 & <e1> . 2 = 0 & <e1> . 3 = 0 )
by FINSEQ_1:62;
A2:
( <e2> . 1 = 0 & <e2> . 2 = 1 & <e2> . 3 = 0 )
by FINSEQ_1:62;
A3:
( <e3> . 1 = 0 & <e3> . 2 = 0 & <e3> . 3 = 1 )
by FINSEQ_1:62;
A4:
(p1 + p2) . 1 = (p1 . 1) + (p2 . 1)
by RVSUM_1:27;
A5:
(p1 + p2) . 2 = (p1 . 2) + (p2 . 2)
by RVSUM_1:27;
A6:
(p1 + p2) . 3 = (p1 . 3) + (p2 . 3)
by RVSUM_1:27;
A0: ((((p1 + p2) . 1) * <e1> ) + (((p1 + p2) . 2) * <e2> )) + (((p1 + p2) . 3) * <e3> ) =
(|[(((p1 + p2) . 1) * 1),(((p1 + p2) . 1) * 0 ),(((p1 + p2) . 1) * 0 )]| + (((p1 + p2) . 2) * <e2> )) + (((p1 + p2) . 3) * <e3> )
by A1, Lm3
.=
(|[((p1 + p2) . 1),0 ,0 ]| + |[(((p1 + p2) . 2) * 0 ),(((p1 + p2) . 2) * 1),(((p1 + p2) . 2) * 0 )]|) + (((p1 + p2) . 3) * <e3> )
by A2, Lm3
.=
(|[((p1 + p2) . 1),0 ,0 ]| + |[0 ,((p1 + p2) . 2),0 ]|) + |[(((p1 + p2) . 3) * 0 ),(((p1 + p2) . 3) * 0 ),(((p1 + p2) . 3) * 1)]|
by A3, Lm3
.=
(|[((p1 + p2) . 1),0 ,0 ]| + |[0 ,((p1 + p2) . 2),0 ]|) + |[0 ,0 ,((p1 + p2) . 3)]|
;
A7:
( |[((p1 + p2) . 1),0 ,0 ]| . 1 = (p1 + p2) . 1 & |[((p1 + p2) . 1),0 ,0 ]| . 2 = 0 & |[((p1 + p2) . 1),0 ,0 ]| . 3 = 0 )
by FINSEQ_1:62;
A8:
( |[0 ,((p1 + p2) . 2),0 ]| . 1 = 0 & |[0 ,((p1 + p2) . 2),0 ]| . 2 = (p1 + p2) . 2 & |[0 ,((p1 + p2) . 2),0 ]| . 3 = 0 )
by FINSEQ_1:62;
A9:
( |[0 ,0 ,((p1 + p2) . 3)]| . 1 = 0 & |[0 ,0 ,((p1 + p2) . 3)]| . 2 = 0 & |[0 ,0 ,((p1 + p2) . 3)]| . 3 = (p1 + p2) . 3 )
by FINSEQ_1:62;
A10: ((((p1 + p2) . 1) * <e1> ) + (((p1 + p2) . 2) * <e2> )) + (((p1 + p2) . 3) * <e3> ) =
|[(((p1 + p2) . 1) + 0 ),(0 + ((p1 + p2) . 2)),(0 + 0 )]| + |[0 ,0 ,((p1 + p2) . 3)]|
by A0, A7, A8, Lm4
.=
|[((p1 + p2) . 1),((p1 + p2) . 2),0 ]| + |[0 ,0 ,((p1 + p2) . 3)]|
;
A11:
( |[((p1 + p2) . 1),((p1 + p2) . 2),0 ]| . 1 = (p1 + p2) . 1 & |[((p1 + p2) . 1),((p1 + p2) . 2),0 ]| . 2 = (p1 + p2) . 2 & |[((p1 + p2) . 1),((p1 + p2) . 2),0 ]| . 3 = 0 )
by FINSEQ_1:62;
((((p1 + p2) . 1) * <e1> ) + (((p1 + p2) . 2) * <e2> )) + (((p1 + p2) . 3) * <e3> ) =
|[(((p1 + p2) . 1) + 0 ),(((p1 + p2) . 2) + 0 ),(0 + ((p1 + p2) . 3))]|
by A9, A10, A11, Lm4
.=
|[((p1 + p2) . 1),((p1 + p2) . 2),((p1 + p2) . 3)]|
;
hence
p1 + p2 = ((((p1 . 1) + (p2 . 1)) * <e1> ) + (((p1 . 2) + (p2 . 2)) * <e2> )) + (((p1 . 3) + (p2 . 3)) * <e3> )
by A4, A5, A6, Lm1; verum