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:59;
A2: Im (((p1 `1 ) + (p2 `1 )) + (((p1 `2 ) + (p2 `2 )) * <i> )) = (p1 `2 ) + (p2 `2 ) by COMPLEX1:28;
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:28;
Re (((p1 + p2) `1 ) + (((p1 + p2) `2 ) * <i> )) = (p1 + p2) `1 by COMPLEX1:28;
then Re (((p1 + p2) `1 ) + (((p1 + p2) `2 ) * <i> )) = (p1 `1 ) + (p2 `1 ) by A1, EUCLID:56;
hence ((p1 + p2) `1 ) + (((p1 + p2) `2 ) * <i> ) = ((p1 `1 ) + (p2 `1 )) + (((p1 `2 ) + (p2 `2 )) * <i> ) by A1, A3, A2, COMPLEX1:9, EUCLID:56; :: thesis: verum