let p1, p2, g1, g2 be Element of 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:28
.= p2 - (g2 * <i> ) by COMPLEX1:28
.= p2 + ((- g2) * <i> ) ; :: thesis: verum