let z be Quaternion; :: thesis: z = (((Rea z) + ((Im1 z) * <i>)) + ((Im2 z) * <j>)) + ((Im3 z) * <k>)
[*(Rea z),(Im1 z),(Im2 z),(Im3 z)*] = z by Th17;
hence z = (((Rea z) + ((Im1 z) * <i>)) + ((Im2 z) * <j>)) + ((Im3 z) * <k>) by Lm19; :: thesis: verum