let p1, p2 be Point of (TOP-REAL 2); :: thesis: p1 - p2 = |[((p1 `1 ) - (p2 `1 )),((p1 `2 ) - (p2 `2 ))]|
- p2 = |[(- (p2 `1 )),(- (p2 `2 ))]| by Th63;
then ( (- p2) `1 = - (p2 `1 ) & (- p2) `2 = - (p2 `2 ) ) by FINSEQ_1:61;
hence p1 - p2 = |[((p1 `1 ) + (- (p2 `1 ))),((p1 `2 ) + (- (p2 `2 )))]| by Th59
.= |[((p1 `1 ) - (p2 `1 )),((p1 `2 ) - (p2 `2 ))]| ;
:: thesis: verum