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;

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;

A8: now :: thesis: not a = 0

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 A10: a " <> 0 by XCMPLX_1:202;
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