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 Th8;
hence euc2cpx (p1 + p2) = (euc2cpx p1) + (euc2cpx p2) ; :: thesis: verum