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