let x, y, z, w be Real; [*x,y,z,w*] = ((x + (y * <i>)) + (z * <j>)) + (w * <k>)
reconsider x0 = x + 0, y0 = y + 0 as Element of REAL by XREAL_0:def 1;
<i> = [*(In (0,REAL)),jj*]
by ARYTM_0:def 5;
then
<i> = [*0,jj,0,0*]
by QUATERNI:91;
then A1: y * <i> =
[*(y * 0),(y * jj),(y * 0),(y * 0)*]
by QUATERNI:def 21
.=
[*0,y,0,0*]
;
A2: z * <j> =
[*(z * 0),(z * 0),(z * jj),(y * 0)*]
by QUATERNI:def 21
.=
[*0,0,z,0*]
;
A3: w * <k> =
[*(w * 0),(w * 0),(w * 0),(w * jj)*]
by QUATERNI:def 21
.=
[*0,0,0,w*]
;
x + (y * <i>) =
[*x0,y0,0,0*]
by A1, QUATERNI:def 19
.=
[*x,y,0,0*]
;
then (x + (y * <i>)) + (z * <j>) =
[*x0,y0,(0 + z),(0 + 0)*]
by A2, QUATERNI:def 7
.=
[*x,y,z,0*]
;
then
((x + (y * <i>)) + (z * <j>)) + (w * <k>) = [*x0,y0,(0 + z),(0 + w)*]
by A3, QUATERNI:def 7;
hence
[*x,y,z,w*] = ((x + (y * <i>)) + (z * <j>)) + (w * <k>)
; verum