let n be Nat; :: thesis: for p1, p2 being Point of (TOP-REAL n)
for r1, r2 being Real holds
( not ((1 - r1) * p1) + (r1 * p2) = ((1 - r2) * p1) + (r2 * p2) or r1 = r2 or p1 = p2 )
let p1, p2 be Point of (TOP-REAL n); :: thesis: for r1, r2 being Real holds
( not ((1 - r1) * p1) + (r1 * p2) = ((1 - r2) * p1) + (r2 * p2) or r1 = r2 or p1 = p2 )
let r1, r2 be Real; :: thesis: ( not ((1 - r1) * p1) + (r1 * p2) = ((1 - r2) * p1) + (r2 * p2) or r1 = r2 or p1 = p2 )
assume A1: ((1 - r1) * p1) + (r1 * p2) = ((1 - r2) * p1) + (r2 * p2) ; :: thesis: ( r1 = r2 or p1 = p2 )
A2: (1 * p1) + ((- (r1 * p1)) + (r1 * p2)) = ((1 * p1) + (- (r1 * p1))) + (r1 * p2) by RLVECT_1:def 3
.= ((1 * p1) - (r1 * p1)) + (r1 * p2)
.= ((1 - r2) * p1) + (r2 * p2) by A1, RLVECT_1:35
.= ((1 * p1) - (r2 * p1)) + (r2 * p2) by RLVECT_1:35
.= ((1 * p1) + (- (r2 * p1))) + (r2 * p2)
.= (1 * p1) + ((- (r2 * p1)) + (r2 * p2)) by RLVECT_1:def 3 ;
A3: ((r2 - r1) * p1) + (r1 * p2) = ((r2 * p1) - (r1 * p1)) + (r1 * p2) by RLVECT_1:35
.= ((r2 * p1) + (- (r1 * p1))) + (r1 * p2)
.= (r2 * p1) + ((- (r1 * p1)) + (r1 * p2)) by RLVECT_1:def 3
.= (r2 * p1) + ((- (r2 * p1)) + (r2 * p2)) by A2, GOBOARD7:4
.= ((r2 * p1) + (- (r2 * p1))) + (r2 * p2) by RLVECT_1:def 3
.= (0. (TOP-REAL n)) + (r2 * p2) by RLVECT_1:5
.= r2 * p2 by RLVECT_1:4 ;
(r2 - r1) * p1 = ((r2 - r1) * p1) + (0. (TOP-REAL n)) by RLVECT_1:4
.= ((r2 - r1) * p1) + ((r1 * p2) - (r1 * p2)) by RLVECT_1:5
.= (r2 * p2) - (r1 * p2) by A3, RLVECT_1:def 3
.= (r2 - r1) * p2 by RLVECT_1:35 ;
then ( r2 - r1 = 0 or p1 = p2 ) by RLVECT_1:36;
hence ( r1 = r2 or p1 = p2 ) ; :: thesis: verum