let n be Nat; :: thesis: for p, q being Point of (TOP-REAL n)
for r being Real st 0 < r & p = ((1 - r) * p) + (r * q) holds
p = q
let p, q be Point of (TOP-REAL n); :: thesis: for r being Real st 0 < r & p = ((1 - r) * p) + (r * q) holds
p = q
let r be Real; :: thesis: ( 0 < r & p = ((1 - r) * p) + (r * q) implies p = q )
assume that
A1: 0 < r and
A2: p = ((1 - r) * p) + (r * q) ; :: thesis: p = q
A3: ((1 - r) * p) + (r * p) = ((1 - r) + r) * p by RLVECT_1:def 6
.= p by RLVECT_1:def 8 ;
r * p = (r * p) + (0. (TOP-REAL n)) by RLVECT_1:4
.= (r * p) + (((1 - r) * p) + (- ((1 - r) * p))) by RLVECT_1:5
.= ((r * q) + ((1 - r) * p)) + (- ((1 - r) * p)) by A2, A3, RLVECT_1:def 3
.= (r * q) + (((1 - r) * p) + (- ((1 - r) * p))) by RLVECT_1:def 3
.= (r * q) + (0. (TOP-REAL n)) by RLVECT_1:5
.= r * q by RLVECT_1:4 ;
hence p = q by A1, RLVECT_1:36; :: thesis: verum