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

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