let p1, p2 be Point of (TOP-REAL 2); :: thesis: euc2cpx (p1 + p2) = (euc2cpx p1) + (euc2cpx p2)
euc2cpx (p1 + p2) = ((p1 `1 ) + (p2 `1 )) + (((p1 `2 ) + (p2 `2 )) * <i> ) by Th12;
hence euc2cpx (p1 + p2) = (euc2cpx p1) + (euc2cpx p2) ; :: thesis: verum