let r, s be Real; :: thesis: for V being RealLinearSpace
for v being VECTOR of V
for L1, L2 being Linear_Combination of V st L1 . v <> L2 . v holds
( ((r * L1) + ((1 - r) * L2)) . v = s iff r = ((L2 . v) - s) / ((L2 . v) - (L1 . v)) )
let V be RealLinearSpace; :: thesis: for v being VECTOR of V
for L1, L2 being Linear_Combination of V st L1 . v <> L2 . v holds
( ((r * L1) + ((1 - r) * L2)) . v = s iff r = ((L2 . v) - s) / ((L2 . v) - (L1 . v)) )
let v be VECTOR of V; :: thesis: for L1, L2 being Linear_Combination of V st L1 . v <> L2 . v holds
( ((r * L1) + ((1 - r) * L2)) . v = s iff r = ((L2 . v) - s) / ((L2 . v) - (L1 . v)) )
let L1, L2 be Linear_Combination of V; :: thesis: ( L1 . v <> L2 . v implies ( ((r * L1) + ((1 - r) * L2)) . v = s iff r = ((L2 . v) - s) / ((L2 . v) - (L1 . v)) ) )
set u1 = L1 . v;
set u2 = L2 . v;
A1: ((r * L1) + ((1 - r) * L2)) . v = ((r * L1) . v) + (((1 - r) * L2) . v) by RLVECT_2:def 10
.= (r * (L1 . v)) + (((1 - r) * L2) . v) by RLVECT_2:def 11
.= (r * (L1 . v)) + (((- r) + 1) * (L2 . v)) by RLVECT_2:def 11
.= (r * ((L1 . v) - (L2 . v))) + (L2 . v) ;
assume A2: L1 . v <> L2 . v ; :: thesis: ( ((r * L1) + ((1 - r) * L2)) . v = s iff r = ((L2 . v) - s) / ((L2 . v) - (L1 . v)) )
then A3: (L1 . v) - (L2 . v) <> 0 ;
A4: (L2 . v) - (L1 . v) <> 0 by A2;

hereby :: thesis: ( r = ((L2 . v) - s) / ((L2 . v) - (L1 . v)) implies ((r * L1) + ((1 - r) * L2)) . v = s )

assume ((r * L1) + ((1 - r) * L2)) . v = s ; :: thesis: r = ((L2 . v) - s) / ((L2 . v) - (L1 . v))
then r * ((L2 . v) - (L1 . v)) = ((L2 . v) - s) * 1 by A1;
then r / 1 = ((L2 . v) - s) / ((L2 . v) - (L1 . v)) by A4, XCMPLX_1:94;
hence r = ((L2 . v) - s) / ((L2 . v) - (L1 . v)) ; :: thesis: verum

end;

assume r = ((L2 . v) - s) / ((L2 . v) - (L1 . v)) ; :: thesis: ((r * L1) + ((1 - r) * L2)) . v = s
hence ((r * L1) + ((1 - r) * L2)) . v = ((((L2 . v) - s) / (- ((L1 . v) - (L2 . v)))) * ((L1 . v) - (L2 . v))) + (L2 . v) by A1
.= (((- ((L2 . v) - s)) / ((L1 . v) - (L2 . v))) * ((L1 . v) - (L2 . v))) + (L2 . v) by XCMPLX_1:192
.= (- ((L2 . v) - s)) + (L2 . v) by A3, XCMPLX_1:87
.= s ;
:: thesis: verum