let x, y, z, w be Real; :: thesis: [*x,y,z,w*] = ((x + (y * <i> )) + (z * <j> )) + (w * <k> )
<i> = [*0 ,1*] by ARYTM_0:def 7;
then A1: <i> = [*0 ,1,0 ,0 *] by QUATERNI:def 6, QUATERNI:91;
A2: y * <i> = [*(y * 0 ),(y * 1),(y * 0 ),(y * 0 )*] by A1, QUATERNI:def 21
.= [*0 ,y,0 ,0 *] ;
A3: z * <j> = [*(z * 0 ),(z * 0 ),(z * 1),(y * 0 )*] by QUATERNI:def 21
.= [*0 ,0 ,z,0 *] ;
A4: w * <k> = [*(w * 0 ),(w * 0 ),(w * 0 ),(w * 1)*] by QUATERNI:def 21
.= [*0 ,0 ,0 ,w*] ;
x + (y * <i> ) = [*(x + 0 ),y,0 ,0 *] by A2, QUATERNI:def 19
.= [*x,y,0 ,0 *] ;
then (x + (y * <i> )) + (z * <j> ) = [*(x + 0 ),(y + 0 ),(0 + z),(0 + 0 )*] by A3, QUATERNI:def 7
.= [*x,y,z,0 *] ;
then ((x + (y * <i> )) + (z * <j> )) + (w * <k> ) = [*(x + 0 ),(y + 0 ),(0 + z),(0 + w)*] by A4, QUATERNI:def 7;
hence [*x,y,z,w*] = ((x + (y * <i> )) + (z * <j> )) + (w * <k> ) ; :: thesis: verum