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