let n be Nat; :: thesis: for p, p1, q being Point of (TOP-REAL n) st p + p1 = q + p1 holds

p = q

let p, p1, q be Point of (TOP-REAL n); :: thesis: ( p + p1 = q + p1 implies p = q )

assume A1: p + p1 = q + p1 ; :: thesis: p = q

thus p = p + (0. (TOP-REAL n)) by RLVECT_1:4

.= p + (p1 - p1) by RLVECT_1:5

.= (p + p1) - p1 by RLVECT_1:def 3

.= q + (p1 - p1) by A1, RLVECT_1:def 3

.= q + (0. (TOP-REAL n)) by RLVECT_1:5

.= q by RLVECT_1:4 ; :: thesis: verum

p = q

let p, p1, q be Point of (TOP-REAL n); :: thesis: ( p + p1 = q + p1 implies p = q )

assume A1: p + p1 = q + p1 ; :: thesis: p = q

thus p = p + (0. (TOP-REAL n)) by RLVECT_1:4

.= p + (p1 - p1) by RLVECT_1:5

.= (p + p1) - p1 by RLVECT_1:def 3

.= q + (p1 - p1) by A1, RLVECT_1:def 3

.= q + (0. (TOP-REAL n)) by RLVECT_1:5

.= q by RLVECT_1:4 ; :: thesis: verum