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 & 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
A3: a * (u - y) = b * (v - y) and
A4: ( a <> 0 or b <> 0 ) by ANALMETR:18;
take r = (a " ) * b; :: thesis: ( u - y = r * (v - y) & r <> 0 )

A5: now

assume a = 0 ; :: thesis: contradiction
then ( 0. V = b * (v - y) & b <> 0 ) by A3, A4, RLVECT_1:23;
then v - y = 0. V by RLVECT_1:24;
hence contradiction by A2, RLVECT_1:35; :: thesis: verum

end;

A6: now

assume b = 0 ; :: thesis: contradiction
then ( 0. V = a * (u - y) & a <> 0 ) by A3, A4, RLVECT_1:23;
then u - y = 0. V by RLVECT_1:24;
hence contradiction by A2, RLVECT_1:35; :: thesis: verum

end;

A7: a " <> 0 by A5, XCMPLX_1:203;
u - y = r * (v - y)

proof

thus r * (v - y) = (a " ) * (a * (u - y)) by A3, RLVECT_1:def 9
.= ((a " ) * a) * (u - y) by RLVECT_1:def 9
.= 1 * (u - y) by A5, XCMPLX_0:def 7
.= u - y by RLVECT_1:def 9 ; :: thesis: verum

end;

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