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