let n be Nat; :: thesis: for p, p1 being Point of (TOP-REAL n) holds
( p = (p + p1) - p1 & p = (p - p1) + p1 )
let p, p1 be Point of (TOP-REAL n); :: thesis: ( p = (p + p1) - p1 & p = (p - p1) + p1 )
thus p = p + (0.REAL n) by RVSUM_1:33
.= p + (p1 - p1) by RVSUM_1:58
.= (p + p1) - p1 by Th49 ; :: thesis: p = (p - p1) + p1
hence p = p + (p1 - p1) by Th49
.= p + ((- p1) + p1)
.= (p - p1) + p1 by FINSEQOP:29 ;
:: thesis: verum