let V be RealLinearSpace; :: thesis: for y, u, v being VECTOR of V st y,u '||' y,v & y <> u & y <> v holds

ex r being Real st

( u - y = r * (v - y) & r <> 0 )

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

( u - y = r * (v - y) & r <> 0 ) )

assume that

A1: y,u '||' y,v and

A2: y <> u and

A3: y <> v ; :: thesis: ex r being Real st

( u - y = r * (v - y) & r <> 0 )

( y,u // y,v or y,u // v,y ) by A1, GEOMTRAP:def 1;

then consider a, b being Real such that

A4: a * (u - y) = b * (v - y) and

A5: ( a <> 0 or b <> 0 ) by ANALMETR:14;

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

r * (v - y) = (a ") * (a * (u - y)) by A4, RLVECT_1:def 7

.= ((a ") * a) * (u - y) by RLVECT_1:def 7

.= 1 * (u - y) by A8, XCMPLX_0:def 7

.= u - y by RLVECT_1:def 8 ;

hence ( u - y = r * (v - y) & r <> 0 ) by A6, A10, XCMPLX_1:6; :: thesis: verum

ex r being Real st

( u - y = r * (v - y) & r <> 0 )

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

( u - y = r * (v - y) & r <> 0 ) )

assume that

A1: y,u '||' y,v and

A2: y <> u and

A3: y <> v ; :: thesis: ex r being Real st

( u - y = r * (v - y) & r <> 0 )

( y,u // y,v or y,u // v,y ) by A1, GEOMTRAP:def 1;

then consider a, b being Real such that

A4: a * (u - y) = b * (v - y) and

A5: ( a <> 0 or b <> 0 ) by ANALMETR:14;

A6: now :: thesis: not b = 0

assume A7:
b = 0
; :: thesis: contradiction

then 0. V = a * (u - y) by A4, RLVECT_1:10;

then u - y = 0. V by A5, A7, RLVECT_1:11;

hence contradiction by A2, RLVECT_1:21; :: thesis: verum

end;then 0. V = a * (u - y) by A4, RLVECT_1:10;

then u - y = 0. V by A5, A7, RLVECT_1:11;

hence contradiction by A2, RLVECT_1:21; :: thesis: verum

A8: now :: thesis: not a = 0

then A10:
a " <> 0
by XCMPLX_1:202;assume A9:
a = 0
; :: thesis: contradiction

then 0. V = b * (v - y) by A4, RLVECT_1:10;

then v - y = 0. V by A5, A9, RLVECT_1:11;

hence contradiction by A3, RLVECT_1:21; :: thesis: verum

end;then 0. V = b * (v - y) by A4, RLVECT_1:10;

then v - y = 0. V by A5, A9, RLVECT_1:11;

hence contradiction by A3, RLVECT_1:21; :: thesis: verum

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

r * (v - y) = (a ") * (a * (u - y)) by A4, RLVECT_1:def 7

.= ((a ") * a) * (u - y) by RLVECT_1:def 7

.= 1 * (u - y) by A8, XCMPLX_0:def 7

.= u - y by RLVECT_1:def 8 ;

hence ( u - y = r * (v - y) & r <> 0 ) by A6, A10, XCMPLX_1:6; :: thesis: verum