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 )
;
A2:
( <e2> . 1 = 0 & <e2> . 2 = 1 & <e2> . 3 = 0 )
;
A3:
( <e3> . 1 = 0 & <e3> . 2 = 0 & <e3> . 3 = 1 )
;
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;
A7: ((((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, Lm1
.=
(|[((p1 - p2) . 1),0,0]| + |[(((p1 - p2) . 2) * 0),(((p1 - p2) . 2) * 1),(((p1 - p2) . 2) * 0)]|) + (((p1 - p2) . 3) * <e3>)
by A2, Lm1
.=
(|[((p1 - p2) . 1),0,0]| + |[0,((p1 - p2) . 2),0]|) + |[(((p1 - p2) . 3) * 0),(((p1 - p2) . 3) * 0),(((p1 - p2) . 3) * 1)]|
by A3, Lm1
.=
(|[((p1 - p2) . 1),0,0]| + |[0,((p1 - p2) . 2),0]|) + |[0,0,((p1 - p2) . 3)]|
;
A8:
( |[((p1 - p2) . 1),0,0]| . 1 = (p1 - p2) . 1 & |[((p1 - p2) . 1),0,0]| . 2 = 0 & |[((p1 - p2) . 1),0,0]| . 3 = 0 )
;
A9:
( |[0,((p1 - p2) . 2),0]| . 1 = 0 & |[0,((p1 - p2) . 2),0]| . 2 = (p1 - p2) . 2 & |[0,((p1 - p2) . 2),0]| . 3 = 0 )
;
A10:
( |[0,0,((p1 - p2) . 3)]| . 1 = 0 & |[0,0,((p1 - p2) . 3)]| . 2 = 0 & |[0,0,((p1 - p2) . 3)]| . 3 = (p1 - p2) . 3 )
;
A11: ((((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 A7, A8, A9, Lm2
.=
|[((p1 - p2) . 1),((p1 - p2) . 2),0]| + |[0,0,((p1 - p2) . 3)]|
;
( |[((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 )
;
then ((((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 A10, A11, Lm2
.=
|[((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, Th1; verum