let p1, p2, g1, g2 be Real; :: thesis: ( (p1 + (g1 * <i>)) * (p2 + (g2 * <i>)) = ((p1 * p2) - (g1 * g2)) + (((p1 * g2) + (p2 * g1)) * <i>) & (p2 + (g2 * <i>)) *' = p2 + ((- g2) * <i>) )
thus (p1 + (g1 * <i>)) * (p2 + (g2 * <i>)) = ((p1 * p2) - (g1 * g2)) + (((p1 * g2) + (p2 * g1)) * <i>) ; :: thesis: (p2 + (g2 * <i>)) *' = p2 + ((- g2) * <i>)
thus (p2 + (g2 * <i>)) *' = p2 - ((Im (p2 + (g2 * <i>))) * <i>) by COMPLEX1:12
.= p2 - (g2 * <i>) by COMPLEX1:12
.= p2 + ((- g2) * <i>) ; :: thesis: verum