theorem :: QUATERNI:37

for z being Quaternion holds z = (((Rea z) + ((Im1 z) * <i>)) + ((Im2 z) * <j>)) + ((Im3 z) * <k>)