assume p <> w ; :: thesis: ex y being VECTOR of V st
( u,p // p,y & u,v // w,y )
then consider a, b being Real such that
A3: a * (p - v) = b * (w - p) and
A4: 0 < a and
A5: 0 < b by A1;
set y = (((b ") * a) * (p - u)) + p;
A6: ((((b ") * a) * (p - u)) + p) - p = ((b ") * a) * (p - u) by RLSUB_2:61
.= (b ") * (a * (p - u)) by RLVECT_1:def 7 ;
A7: ((((b ") * a) * (p - u)) + p) - w = (((((b ") * a) * (p - u)) + p) - p) + (p - w) by Th1
.= (((((b ") * a) * (p - u)) + p) - p) - (w - p) by RLVECT_1:33 ;
v - u = (p - u) + (v - p) by Th1
.= (p - u) - (p - v) by RLVECT_1:33 ;
then a * (v - u) = (a * (p - u)) - (a * (p - v)) by RLVECT_1:34
.= (b * (((((b ") * a) * (p - u)) + p) - p)) - (b * (w - p)) by A3, A5, A6, Th6
.= b * (((((b ") * a) * (p - u)) + p) - w) by A7, RLVECT_1:34 ;
then A8: u,v // w,(((b ") * a) * (p - u)) + p by A4, A5;
0 < b " by A5;
then A9: 0 < (b ") * a by A4, XREAL_1:129;
jj * (((((b ") * a) * (p - u)) + p) - p) = ((((b ") * a) * (p - u)) + p) - p by RLVECT_1:def 8
.= ((b ") * a) * (p - u) by RLSUB_2:61 ;
then u,p // p,(((b ") * a) * (p - u)) + p by A9;
hence ex y being VECTOR of V st
( u,p // p,y & u,v // w,y ) by A8; :: thesis: verum

assume A10: p = w ; :: thesis: ex y being VECTOR of V st
( u,p // p,y & u,v // w,y )
take y = p; :: thesis: ( u,p // p,y & u,v // w,y )
thus ( u,p // p,y & u,v // w,y ) by A10; :: thesis: verum