let z be Complex; :: thesis: (Re z) + ((Im z) * <i>) = z
[*(Re z),(Im z)*] = z by Lm3;
hence (Re z) + ((Im z) * <i>) = z by Lm21; :: thesis: verum