let x, y, z, w be Real; [*x,y,z,w*] = ((x + (y * <i>)) + (z * <j>)) + (w * <k>)
<i> = [*zz,jj,zz,zz*]
by Lm2, Lm3;
then A1: y * <i> =
[*(y * 0),(y * 1),(y * 0),(y * 0)*]
by Def20
.=
[*0,y,0,0*]
;
A2: z * <j> =
[*(z * 0),(z * 0),(z * 1),(y * 0)*]
by Def20
.=
[*0,0,z,0*]
;
A3: w * <k> =
[*(w * 0),(w * 0),(w * 0),(w * 1)*]
by Def20
.=
[*0,0,0,w*]
;
x + (y * <i>) =
[*(x + 0),y,0,0*]
by A1, Def18
.=
[*x,y,0,0*]
;
then (x + (y * <i>)) + (z * <j>) =
[*(x + 0),(y + 0),(0 + z),(0 + 0)*]
by A2, Def6
.=
[*x,y,z,0*]
;
then
((x + (y * <i>)) + (z * <j>)) + (w * <k>) = [*(x + 0),(y + 0),(0 + z),(0 + w)*]
by A3, Def6;
hence
[*x,y,z,w*] = ((x + (y * <i>)) + (z * <j>)) + (w * <k>)
; verum