let V be RealLinearSpace; :: thesis: for v, w being Point of V st 0. V in LSeg (v,w) holds
ex r being Real st
( v = r * w or w = r * v )
let v, w be Point of V; :: thesis: ( 0. V in LSeg (v,w) implies ex r being Real st
( v = r * w or w = r * v ) )
assume 0. V in LSeg (v,w) ; :: thesis: ex r being Real st
( v = r * w or w = r * v )
then consider s being Real such that
A1: 0. V = ((1 - s) * v) + (s * w) and
0 <= s and
s <= 1 ;
- (s * w) = (1 - s) * v by A1, RLVECT_1:6;
then A2: (- s) * w = (1 - s) * v by RLVECT_1:79;

per cases ( - s <> 0 or - s = 0 ) ;

suppose A3: - s <> 0 ; :: thesis: ex r being Real st
( v = r * w or w = r * v )

take r = ((- s) ") * (1 - s); :: thesis: ( v = r * w or w = r * v )
w = 1 * w by RLVECT_1:def 8
.= (((- s) ") * (- s)) * w by A3, XCMPLX_0:def 7
.= ((- s) ") * ((- s) * w) by RLVECT_1:def 7
.= r * v by A2, RLVECT_1:def 7 ;
hence ( v = r * w or w = r * v ) ; :: thesis: verum

end;

suppose A4: - s = 0 ; :: thesis: ex r being Real st
( v = r * w or w = r * v )

take - s ; :: thesis: ( v = (- s) * w or w = (- s) * v )
thus ( v = (- s) * w or w = (- s) * v ) by A2, A4, RLVECT_1:def 8; :: thesis: verum

end;

end;