theorem :: HAHNBAN1:2

for x1, y1, x2, y2 being Real holds (x1 + (y1 * <i>)) * (x2 + (y2 * <i>)) = ((x1 * x2) - (y1 * y2)) + (((x1 * y2) + (x2 * y1)) * <i>) ;