let V be RealLinearSpace; :: thesis: for u, v, w being VECTOR of V st u <> v & w <> v & u,v // v,w holds

ex r being Real st

( v - u = r * (w - v) & 0 < r )

let u, v, w be VECTOR of V; :: thesis: ( u <> v & w <> v & u,v // v,w implies ex r being Real st

( v - u = r * (w - v) & 0 < r ) )

assume ( u <> v & w <> v & u,v // v,w ) ; :: thesis: ex r being Real st

( v - u = r * (w - v) & 0 < r )

then consider a, b being Real such that

A1: a * (v - u) = b * (w - v) and

A2: 0 < a and

A3: 0 < b by ANALOAF:7;

take r = (a ") * b; :: thesis: ( v - u = r * (w - v) & 0 < r )

0 < a " by A2, XREAL_1:122;

then A4: 0 * b < r by A3, XREAL_1:68;

v - u = 1 * (v - u) by RLVECT_1:def 8

.= ((a ") * a) * (v - u) by A2, XCMPLX_0:def 7

.= (a ") * (b * (w - v)) by A1, RLVECT_1:def 7

.= r * (w - v) by RLVECT_1:def 7 ;

hence ( v - u = r * (w - v) & 0 < r ) by A4; :: thesis: verum

ex r being Real st

( v - u = r * (w - v) & 0 < r )

let u, v, w be VECTOR of V; :: thesis: ( u <> v & w <> v & u,v // v,w implies ex r being Real st

( v - u = r * (w - v) & 0 < r ) )

assume ( u <> v & w <> v & u,v // v,w ) ; :: thesis: ex r being Real st

( v - u = r * (w - v) & 0 < r )

then consider a, b being Real such that

A1: a * (v - u) = b * (w - v) and

A2: 0 < a and

A3: 0 < b by ANALOAF:7;

take r = (a ") * b; :: thesis: ( v - u = r * (w - v) & 0 < r )

0 < a " by A2, XREAL_1:122;

then A4: 0 * b < r by A3, XREAL_1:68;

v - u = 1 * (v - u) by RLVECT_1:def 8

.= ((a ") * a) * (v - u) by A2, XCMPLX_0:def 7

.= (a ") * (b * (w - v)) by A1, RLVECT_1:def 7

.= r * (w - v) by RLVECT_1:def 7 ;

hence ( v - u = r * (w - v) & 0 < r ) by A4; :: thesis: verum