let r, s be Real; :: thesis: for V being RealLinearSpace
for w, v1, v2 being VECTOR of V
for A being Subset of V st not w in Affin A & v1 in A & v2 in A & r <> 1 & (r * w) + ((1 - r) * v1) = (s * w) + ((1 - s) * v2) holds
( r = s & v1 = v2 )
let V be RealLinearSpace; :: thesis: for w, v1, v2 being VECTOR of V
for A being Subset of V st not w in Affin A & v1 in A & v2 in A & r <> 1 & (r * w) + ((1 - r) * v1) = (s * w) + ((1 - s) * v2) holds
( r = s & v1 = v2 )
let w, v1, v2 be VECTOR of V; :: thesis: for A being Subset of V st not w in Affin A & v1 in A & v2 in A & r <> 1 & (r * w) + ((1 - r) * v1) = (s * w) + ((1 - s) * v2) holds
( r = s & v1 = v2 )
let A be Subset of V; :: thesis: ( not w in Affin A & v1 in A & v2 in A & r <> 1 & (r * w) + ((1 - r) * v1) = (s * w) + ((1 - s) * v2) implies ( r = s & v1 = v2 ) )
assume that
A1: ( not w in Affin A & v1 in A & v2 in A ) and
A2: r <> 1 and
A3: (r * w) + ((1 - r) * v1) = (s * w) + ((1 - s) * v2) ; :: thesis: ( r = s & v1 = v2 )
r * w = (r * w) + (0. V) by RLVECT_1:10
.= (r * w) + (((1 - r) * v1) - ((1 - r) * v1)) by RLVECT_1:28
.= ((s * w) + ((1 - s) * v2)) - ((1 - r) * v1) by A3, RLVECT_1:42
.= (((1 - s) * v2) - ((1 - r) * v1)) + (s * w) by RLVECT_1:42 ;
then (r * w) - (s * w) = ((1 - s) * v2) - ((1 - r) * v1) by RLVECT_4:1;
then A5: (r - s) * w = ((1 - s) * v2) - ((1 - r) * v1) by RLVECT_1:49;
A6: A c= Affin A by Lm7;

per cases ( r <> s or r = s ) ;

suppose r <> s ; :: thesis: ( r = s & v1 = v2 )

then A7: r - s <> 0 ;
A8: (1 / (r - s)) * (1 - s) = ((r - s) - (r - 1)) / (r - s) by XCMPLX_1:100
.= ((r - s) / (r - s)) - ((r - 1) / (r - s)) by XCMPLX_1:121
.= 1 - ((r - 1) / (r - s)) by A7, XCMPLX_1:60 ;
A9: - ((1 / (r - s)) * (1 - r)) = - ((1 - r) / (r - s)) by XCMPLX_1:100
.= (- (1 - r)) / (r - s) by XCMPLX_1:188 ;
1 = (r - s) * (1 / (r - s)) by A7, XCMPLX_1:107;
then w = ((1 / (r - s)) * (r - s)) * w by RLVECT_1:def 11
.= (1 / (r - s)) * ((r - s) * w) by RLVECT_1:def 10
.= ((1 / (r - s)) * ((1 - s) * v2)) - ((1 / (r - s)) * ((1 - r) * v1)) by A5, RLVECT_1:48
.= (((1 / (r - s)) * (1 - s)) * v2) - ((1 / (r - s)) * ((1 - r) * v1)) by RLVECT_1:def 10
.= (((1 / (r - s)) * (1 - s)) * v2) - (((1 / (r - s)) * (1 - r)) * v1) by RLVECT_1:def 10
.= (((1 / (r - s)) * (1 - s)) * v2) + (- (((1 / (r - s)) * (1 - r)) * v1)) by RLVECT_1:def 14
.= ((1 - ((r - 1) / (r - s))) * v2) + (((r - 1) / (r - s)) * v1) by A8, A9, RLVECT_4:6 ;
hence ( r = s & v1 = v2 ) by A1, A6, RUSUB_4:def 5; :: thesis: verum

end;

suppose A10: r = s ; :: thesis: ( r = s & v1 = v2 )

A11: 1 - r <> 0 by A2;
(1 - r) * v1 = (1 - r) * v2 by A3, A10, RLVECT_1:21;
hence ( r = s & v1 = v2 ) by A10, A11, RLVECT_1:50; :: thesis: verum

end;

end;