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)*> ) )
A1: ( |[r1,s1]| `1 = r1 & |[r1,s1]| `2 = s1 ) by EUCLID:52;
A2: ( |[r2,s2]| `1 = r2 & |[r2,s2]| `2 = s2 ) by EUCLID:52;
assume ( p1 = <*r1,s1*> & p2 = <*r2,s2*> ) ; :: thesis: ( p1 + p2 = <*(r1 + r2),(s1 + s2)*> & p1 - p2 = <*(r1 - r2),(s1 - s2)*> )
hence ( p1 + p2 = <*(r1 + r2),(s1 + s2)*> & p1 - p2 = <*(r1 - r2),(s1 - s2)*> ) by A1, A2, EUCLID:55, EUCLID:61; :: thesis: verum