let x, y, z, w be Real; :: thesis: [*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>) ; :: thesis: verum