theorem Th1: :: QUATERN2:1

for x, y, z, w being Real holds [*x,y,z,w*] = ((x + (y * <i>)) + (z * <j>)) + (w * <k>)