let r, s be Real; :: thesis: for V being RealLinearSpace
for v, u being VECTOR of V
for I being affinely-independent Subset of V
for p1, p2, w1, w2 being Element of V st v in conv I & u in conv I & not u in conv (I \ {p1}) & not u in conv (I \ {p2}) & w1 in conv (I \ {p1}) & w2 in conv (I \ {p2}) & (r * u) + ((1 - r) * w1) = v & (s * u) + ((1 - s) * w2) = v & r < 1 & s < 1 holds
( w1 = w2 & r = s )
let V be RealLinearSpace; :: thesis: for v, u being VECTOR of V
for I being affinely-independent Subset of V
for p1, p2, w1, w2 being Element of V st v in conv I & u in conv I & not u in conv (I \ {p1}) & not u in conv (I \ {p2}) & w1 in conv (I \ {p1}) & w2 in conv (I \ {p2}) & (r * u) + ((1 - r) * w1) = v & (s * u) + ((1 - s) * w2) = v & r < 1 & s < 1 holds
( w1 = w2 & r = s )
let v, u be VECTOR of V; :: thesis: for I being affinely-independent Subset of V
for p1, p2, w1, w2 being Element of V st v in conv I & u in conv I & not u in conv (I \ {p1}) & not u in conv (I \ {p2}) & w1 in conv (I \ {p1}) & w2 in conv (I \ {p2}) & (r * u) + ((1 - r) * w1) = v & (s * u) + ((1 - s) * w2) = v & r < 1 & s < 1 holds
( w1 = w2 & r = s )
let I be affinely-independent Subset of V; :: thesis: for p1, p2, w1, w2 being Element of V st v in conv I & u in conv I & not u in conv (I \ {p1}) & not u in conv (I \ {p2}) & w1 in conv (I \ {p1}) & w2 in conv (I \ {p2}) & (r * u) + ((1 - r) * w1) = v & (s * u) + ((1 - s) * w2) = v & r < 1 & s < 1 holds
( w1 = w2 & r = s )
let p1, p2, w1, w2 be Element of V; :: thesis: ( v in conv I & u in conv I & not u in conv (I \ {p1}) & not u in conv (I \ {p2}) & w1 in conv (I \ {p1}) & w2 in conv (I \ {p2}) & (r * u) + ((1 - r) * w1) = v & (s * u) + ((1 - s) * w2) = v & r < 1 & s < 1 implies ( w1 = w2 & r = s ) )
assume that
A1: v in conv I and
A2: u in conv I and
A3: not u in conv (I \ {p1}) and
A4: not u in conv (I \ {p2}) and
A5: w1 in conv (I \ {p1}) and
A6: w2 in conv (I \ {p2}) and
A7: (r * u) + ((1 - r) * w1) = v and
A8: (s * u) + ((1 - s) * w2) = v and
A9: r < 1 and
A10: s < 1 ; :: thesis: ( w1 = w2 & r = s )
set Lu = u |-- I;
set Lv = v |-- I;
set Lw1 = w1 |-- I;
set Lw2 = w2 |-- I;
A11: conv I c= Affin I by RLAFFIN1:65;
A12: (u |-- I) . p2 > 0

proof

assume A13: (u |-- I) . p2 <= 0 ; :: thesis: contradiction
(u |-- I) . p2 >= 0 by A2, RLAFFIN1:71;
then for y being set st y in {p2} holds
(u |-- I) . y = 0 by A13, TARSKI:def 1;
hence contradiction by A2, A4, RLAFFIN1:76; :: thesis: verum

end;

conv (I \ {p2}) c= Affin (I \ {p2}) by RLAFFIN1:65;
then w2 |-- I = w2 |-- (I \ {p2}) by A6, RLAFFIN1:77, XBOOLE_1:36;
then Carrier (w2 |-- I) c= I \ {p2} by RLVECT_2:def 6;
then not p2 in Carrier (w2 |-- I) by ZFMISC_1:56;
then A14: (w2 |-- I) . p2 = 0 ;
A15: (u |-- I) . p1 > 0

proof

assume A16: (u |-- I) . p1 <= 0 ; :: thesis: contradiction
(u |-- I) . p1 >= 0 by A2, RLAFFIN1:71;
then for y being set st y in {p1} holds
(u |-- I) . y = 0 by A16, TARSKI:def 1;
hence contradiction by A2, A3, RLAFFIN1:76; :: thesis: verum

end;

conv (I \ {p1}) c= Affin (I \ {p1}) by RLAFFIN1:65;
then w1 |-- I = w1 |-- (I \ {p1}) by A5, RLAFFIN1:77, XBOOLE_1:36;
then Carrier (w1 |-- I) c= I \ {p1} by RLVECT_2:def 6;
then not p1 in Carrier (w1 |-- I) by ZFMISC_1:56;
then A17: (w1 |-- I) . p1 = 0 ;
A18: conv (I \ {p2}) c= conv I by RLAFFIN1:3, XBOOLE_1:36;
then w2 in conv I by A6;
then (s * (u |-- I)) + ((1 - s) * (w2 |-- I)) = v |-- I by A2, A8, A11, RLAFFIN1:70;
then (v |-- I) . p2 = ((s * (u |-- I)) . p2) + (((1 - s) * (w2 |-- I)) . p2) by RLVECT_2:def 10
.= (s * ((u |-- I) . p2)) + (((1 - s) * (w2 |-- I)) . p2) by RLVECT_2:def 11
.= (s * ((u |-- I) . p2)) + ((1 - s) * ((w2 |-- I) . p2)) by RLVECT_2:def 11
.= s * ((u |-- I) . p2) by A14 ;
then A19: (v |-- I) . p2 < 1 * ((u |-- I) . p2) by A10, A12, XREAL_1:68;
then A20: ((u |-- I) . p2) - ((v |-- I) . p2) >= ((v |-- I) . p2) - ((v |-- I) . p2) by XREAL_1:9;
A21: conv (I \ {p1}) c= conv I by RLAFFIN1:3, XBOOLE_1:36;
then (w1 |-- I) . p2 >= 0 by A5, RLAFFIN1:71;
then A22: (1 / (1 - s)) - 0 >= (1 / (1 - s)) - (((w1 |-- I) . p2) / (((u |-- I) . p2) - ((v |-- I) . p2))) by A20, XREAL_1:10;
w1 in conv I by A5, A21;
then v |-- I = (r * (u |-- I)) + ((1 - r) * (w1 |-- I)) by A2, A7, A11, RLAFFIN1:70;
then (v |-- I) . p1 = ((r * (u |-- I)) . p1) + (((1 - r) * (w1 |-- I)) . p1) by RLVECT_2:def 10
.= (r * ((u |-- I) . p1)) + (((1 - r) * (w1 |-- I)) . p1) by RLVECT_2:def 11
.= (r * ((u |-- I) . p1)) + ((1 - r) * ((w1 |-- I) . p1)) by RLVECT_2:def 11
.= r * ((u |-- I) . p1) by A17 ;
then A23: (v |-- I) . p1 < 1 * ((u |-- I) . p1) by A9, A15, XREAL_1:68;
then A24: ((u |-- I) . p1) - ((v |-- I) . p1) >= ((v |-- I) . p1) - ((v |-- I) . p1) by XREAL_1:9;
w2 = ((1 / (1 - s)) * v) + ((1 - (1 / (1 - s))) * u) by A8, A10, Lm1;
then A25: w2 |-- I = ((1 / (1 - s)) * (v |-- I)) + ((1 - (1 / (1 - s))) * (u |-- I)) by A1, A2, A11, RLAFFIN1:70;
then A26: 1 / (1 - s) = (((u |-- I) . p2) - 0) / (((u |-- I) . p2) - ((v |-- I) . p2)) by A14, A19, RLAFFIN1:81;
A27: w1 = ((1 / (1 - r)) * v) + ((1 - (1 / (1 - r))) * u) by A7, A9, Lm1;
then A28: w1 |-- I = ((1 / (1 - r)) * (v |-- I)) + ((1 - (1 / (1 - r))) * (u |-- I)) by A1, A2, A11, RLAFFIN1:70;
then A29: 1 / (1 - r) = (((u |-- I) . p2) - ((w1 |-- I) . p2)) / (((u |-- I) . p2) - ((v |-- I) . p2)) by A19, RLAFFIN1:81
.= (1 / (1 - s)) - (((w1 |-- I) . p2) / (((u |-- I) . p2) - ((v |-- I) . p2))) by A26, XCMPLX_1:120 ;
(w2 |-- I) . p1 >= 0 by A6, A18, RLAFFIN1:71;
then A30: (1 / (1 - r)) - 0 >= (1 / (1 - r)) - (((w2 |-- I) . p1) / (((u |-- I) . p1) - ((v |-- I) . p1))) by A24, XREAL_1:10;
A31: 1 / (1 - r) = (((u |-- I) . p1) - 0) / (((u |-- I) . p1) - ((v |-- I) . p1)) by A17, A23, A28, RLAFFIN1:81;
1 / (1 - s) = (((u |-- I) . p1) - ((w2 |-- I) . p1)) / (((u |-- I) . p1) - ((v |-- I) . p1)) by A23, A25, RLAFFIN1:81
.= (1 / (1 - r)) - (((w2 |-- I) . p1) / (((u |-- I) . p1) - ((v |-- I) . p1))) by A31, XCMPLX_1:120 ;
then 1 - r = 1 - s by A30, A22, A29, XCMPLX_1:59, XXREAL_0:1;
hence ( w1 = w2 & r = s ) by A8, A10, A27, Lm1; :: thesis: verum