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