let V be RealLinearSpace; :: thesis: for u, v, u1, v1 being VECTOR of V holds
( ( u,v // u1,v1 or u,v // v1,u1 ) iff ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) )
let u, v, u1, v1 be VECTOR of V; :: thesis: ( ( u,v // u1,v1 or u,v // v1,u1 ) iff ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) )

A1: now

let w, y, w1, y1 be VECTOR of V; :: thesis: ( w,y // w1,y1 implies ex a, b being Real st
( a * (y - w) = b * (y1 - w1) & ( a <> 0 or b <> 0 ) ) )
assume A2: w,y // w1,y1 ; :: thesis: ex a, b being Real st
( a * (y - w) = b * (y1 - w1) & ( a <> 0 or b <> 0 ) )

A3: now

assume w = y ; :: thesis: ex a, b being Real st
( a * (y - w) = b * (y1 - w1) & ( a <> 0 or b <> 0 ) )
then 1 * (y - w) = 0. V by RLVECT_1:23, RLVECT_1:28
.= 0 * (y1 - w1) by RLVECT_1:23 ;
hence ex a, b being Real st
( a * (y - w) = b * (y1 - w1) & ( a <> 0 or b <> 0 ) ) ; :: thesis: verum

end;

A4: now

assume w1 = y1 ; :: thesis: ex a, b being Real st
( a * (y - w) = b * (y1 - w1) & ( a <> 0 or b <> 0 ) )
then 1 * (y1 - w1) = 0. V by RLVECT_1:23, RLVECT_1:28
.= 0 * (y - w) by RLVECT_1:23 ;
hence ex a, b being Real st
( a * (y - w) = b * (y1 - w1) & ( a <> 0 or b <> 0 ) ) ; :: thesis: verum

end;

( ex a, b being Real st
( 0 < a & 0 < b & a * (y - w) = b * (y1 - w1) ) implies ex a, b being Real st
( a * (y - w) = b * (y1 - w1) & ( a <> 0 or b <> 0 ) ) ) ;
hence ex a, b being Real st
( a * (y - w) = b * (y1 - w1) & ( a <> 0 or b <> 0 ) ) by A2, A3, A4, ANALOAF:def 1; :: thesis: verum

end;

A5: now

assume u,v // v1,u1 ; :: thesis: ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) )
then consider a, b being Real such that
A6: a * (v - u) = b * (u1 - v1) and
A7: ( a <> 0 or b <> 0 ) by A1;
A8: (- b) * (v1 - u1) = b * (- (v1 - u1)) by RLVECT_1:38
.= a * (v - u) by A6, RLVECT_1:47 ;
( a <> 0 or - b <> 0 ) by A7;
hence ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) by A8; :: thesis: verum

end;

A9: now

let w, y, w1, y1 be VECTOR of V; :: thesis: ( ex a, b being Real st
( a * (y - w) = b * (y1 - w1) & a = 0 & b <> 0 ) implies w,y // w1,y1 )
given a, b being Real such that A10: a * (y - w) = b * (y1 - w1) and
A11: ( a = 0 & b <> 0 ) ; :: thesis: w,y // w1,y1
0. V = b * (y1 - w1) by A10, A11, RLVECT_1:23;
then y1 - w1 = 0. V by A11, RLVECT_1:24;
then y1 = w1 by RLVECT_1:35;
hence w,y // w1,y1 by ANALOAF:18; :: thesis: verum

end;

A12: now

let w, y, w1, y1 be VECTOR of V; :: thesis: ( ex a, b being Real st
( a * (y - w) = b * (y1 - w1) & 0 < a & b < 0 ) implies w,y // y1,w1 )
given a, b being Real such that A13: a * (y - w) = b * (y1 - w1) and
A14: ( 0 < a & b < 0 ) ; :: thesis: w,y // y1,w1
A15: 0 < - b by A14, XREAL_1:60;
a * (y - w) = b * (- (w1 - y1)) by A13, RLVECT_1:47
.= (- b) * (w1 - y1) by RLVECT_1:38 ;
hence w,y // y1,w1 by A14, A15, ANALOAF:def 1; :: thesis: verum

end;

now

given a, b being Real such that A16: a * (v - u) = b * (v1 - u1) and
A17: ( a <> 0 or b <> 0 ) ; :: thesis: ( u,v // u1,v1 or u,v // v1,u1 )

A18: now

assume b = 0 ; :: thesis: ( u,v // u1,v1 or u,v // v1,u1 )
then u1,v1 // u,v by A9, A16, A17;
hence ( u,v // u1,v1 or u,v // v1,u1 ) by ANALOAF:21; :: thesis: verum

end;

now

assume A19: ( a <> 0 & b <> 0 ) ; :: thesis: ( u,v // u1,v1 or u,v // v1,u1 )
A20: ( 0 < a & b < 0 & not u,v // u1,v1 implies u,v // v1,u1 ) by A12, A16;

A21: now

assume ( a < 0 & 0 < b ) ; :: thesis: ( u,v // u1,v1 or u,v // v1,u1 )
then u1,v1 // v,u by A12, A16;
then v,u // u1,v1 by ANALOAF:21;
hence ( u,v // u1,v1 or u,v // v1,u1 ) by ANALOAF:21; :: thesis: verum

end;

now

assume ( a < 0 & b < 0 ) ; :: thesis: ( u,v // u1,v1 or u,v // v1,u1 )
then A22: ( 0 < - a & 0 < - b ) by XREAL_1:60;
(- a) * (u - v) = a * (- (u - v)) by RLVECT_1:38
.= b * (v1 - u1) by A16, RLVECT_1:47
.= b * (- (u1 - v1)) by RLVECT_1:47
.= (- b) * (u1 - v1) by RLVECT_1:38 ;
then v,u // v1,u1 by A22, ANALOAF:def 1;
hence ( u,v // u1,v1 or u,v // v1,u1 ) by ANALOAF:21; :: thesis: verum

end;

hence ( u,v // u1,v1 or u,v // v1,u1 ) by A16, A19, A20, A21, ANALOAF:def 1; :: thesis: verum

end;

hence ( u,v // u1,v1 or u,v // v1,u1 ) by A9, A16, A18; :: thesis: verum

end;

hence ( ( u,v // u1,v1 or u,v // v1,u1 ) iff ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) ) by A1, A5; :: thesis: verum