let p1, p2 be Point of (TOP-REAL 2); :: thesis: ((p1 + p2) `1) + (((p1 + p2) `2) * <i>) = ((p1 `1) + (p2 `1)) + (((p1 `2) + (p2 `2)) * <i>)
A1: p1 + p2 = |[((p1 `1) + (p2 `1)),((p1 `2) + (p2 `2))]| by EUCLID:55;
A2: Im (((p1 `1) + (p2 `1)) + (((p1 `2) + (p2 `2)) * <i>)) = (p1 `2) + (p2 `2) by COMPLEX1:12;
A3: ( Im (((p1 + p2) `1) + (((p1 + p2) `2) * <i>)) = (p1 + p2) `2 & Re (((p1 `1) + (p2 `1)) + (((p1 `2) + (p2 `2)) * <i>)) = (p1 `1) + (p2 `1) ) by COMPLEX1:12;
Re (((p1 + p2) `1) + (((p1 + p2) `2) * <i>)) = (p1 + p2) `1 by COMPLEX1:12;
then Re (((p1 + p2) `1) + (((p1 + p2) `2) * <i>)) = (p1 `1) + (p2 `1) by A1, EUCLID:52;
hence ((p1 + p2) `1) + (((p1 + p2) `2) * <i>) = ((p1 `1) + (p2 `1)) + (((p1 `2) + (p2 `2)) * <i>) by A1, A3, A2, EUCLID:52; :: thesis: verum