let A, B be Point of (TOP-REAL 2); :: thesis: ( (A + B) `1 = (A `1) + (B `1) & (A + B) `2 = (A `2) + (B `2) )
A + B = |[((A `1) + (B `1)),((A `2) + (B `2))]| by EUCLID:55;
hence ( (A + B) `1 = (A `1) + (B `1) & (A + B) `2 = (A `2) + (B `2) ) by EUCLID:52; :: thesis: verum