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