let p, q be Point of (TOP-REAL 2); :: thesis: ( (p + q) `1 = (p `1 ) + (q `1 ) & (p + q) `2 = (p `2 ) + (q `2 ) )
p + q = |[((p `1 ) + (q `1 )),((p `2 ) + (q `2 ))]| by EUCLID:59;
hence ( (p + q) `1 = (p `1 ) + (q `1 ) & (p + q) `2 = (p `2 ) + (q `2 ) ) by EUCLID:56; :: thesis: verum