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