let z be quaternion number ; :: thesis: z = (((Rea z) + ((Im1 z) * <i> )) + ((Im2 z) * <j> )) + ((Im3 z) * <k> )
[*(Rea z),(Im1 z),(Im2 z),(Im3 z)*] = z by Th24;
hence z = (((Rea z) + ((Im1 z) * <i> )) + ((Im2 z) * <j> )) + ((Im3 z) * <k> ) by Lm18; :: thesis: verum