let p1, p2 be Point of (TOP-REAL 2); :: thesis: for r1, s1, r2, s2 being real number st p1 = <*r1,s1*> & p2 = <*r2,s2*> holds
( p1 + p2 = <*(r1 + r2),(s1 + s2)*> & p1 - p2 = <*(r1 - r2),(s1 - s2)*> )
let r1, s1, r2, s2 be real number ; :: thesis: ( p1 = <*r1,s1*> & p2 = <*r2,s2*> implies ( p1 + p2 = <*(r1 + r2),(s1 + s2)*> & p1 - p2 = <*(r1 - r2),(s1 - s2)*> ) )
assume A1: ( p1 = <*r1,s1*> & p2 = <*r2,s2*> ) ; :: thesis: ( p1 + p2 = <*(r1 + r2),(s1 + s2)*> & p1 - p2 = <*(r1 - r2),(s1 - s2)*> )
( |[r1,s1]| = <*r1,s1*> & |[r2,s2]| = <*r2,s2*> & |[r1,s1]| `1 = r1 & |[r1,s1]| `2 = s1 & |[r2,s2]| `1 = r2 & |[r2,s2]| `2 = s2 ) by EUCLID:56;
hence ( p1 + p2 = <*(r1 + r2),(s1 + s2)*> & p1 - p2 = <*(r1 - r2),(s1 - s2)*> ) by A1, EUCLID:59, EUCLID:65; :: thesis: verum