let V be RealLinearSpace; :: thesis:
given p, q being VECTOR of V such that A1: for w being VECTOR of V ex a, b being Real st (a * p) + (b * q) = w ; :: thesis:
let u, v, w, y be VECTOR of V; :: thesis:
assume A2: ( not u,v // w,y & not u,v // y,w ) ; :: thesis:
consider r1, s1 being Real such that
A3: (r1 * p) + (s1 * q) = v - u by A1;
consider r2, s2 being Real such that
A4: (r2 * p) + (s2 * q) = y - w by A1;
consider r3, s3 being Real such that
A5: (r3 * p) + (s3 * q) = u - w by A1;
set r = (r1 * s2) - (r2 * s1);

A6: now

assume A7: (r1 * s2) - (r2 * s1) = 0 ; :: thesis:

A8: now

assume A9: r1 = 0 ; :: thesis:
A10: s1 <> 0

proof

assume s1 = 0 ; :: thesis:
then v - u = (0. V) + (0 * q) by A3, A9, RLVECT_1:23
.= (0. V) + (0. V) by RLVECT_1:23
.= 0. V by RLVECT_1:10 ;
then u = v by RLVECT_1:35;
hence contradiction by A2, Def1; :: thesis:

end;

then A11: r2 = 0 by A7, A9, XCMPLX_1:6;
A12: s2 <> 0

proof

assume s2 = 0 ; :: thesis:
then y - w = (0. V) + (0 * q) by A4, A11, RLVECT_1:23
.= (0. V) + (0. V) by RLVECT_1:23
.= 0. V by RLVECT_1:10 ;
then y = w by RLVECT_1:35;
hence contradiction by A2, Def1; :: thesis:

end;

A13: v - u = (0. V) + (s1 * q) by A3, A9, RLVECT_1:23
.= s1 * q by RLVECT_1:10 ;
A14: y - w = (0. V) + (s2 * q) by A4, A11, RLVECT_1:23
.= s2 * q by RLVECT_1:10 ;
A15: (s1 " ) * (v - u) = ((s1 " ) * s1) * q by A13, RLVECT_1:def 9
.= 1 * q by A10, XCMPLX_0:def 7
.= q by RLVECT_1:def 9 ;
(s2 " ) * (y - w) = ((s2 " ) * s2) * q by A14, RLVECT_1:def 9
.= 1 * q by A12, XCMPLX_0:def 7
.= q by RLVECT_1:def 9 ;
then ( (s1 " ) * (v - u) = (s2 " ) * (y - w) & s1 " <> 0 & s2 " <> 0 ) by A10, A12, A15, XCMPLX_1:203;
hence contradiction by A2, Lm1; :: thesis:

end;

A16: now

assume A17: ( r1 <> 0 & r2 = 0 ) ; :: thesis:
s2 <> 0

proof

assume s2 = 0 ; :: thesis:
then y - w = (0. V) + (0 * q) by A4, A17, RLVECT_1:23
.= (0. V) + (0. V) by RLVECT_1:23
.= 0. V by RLVECT_1:10 ;
then y = w by RLVECT_1:35;
hence contradiction by A2, Def1; :: thesis:

end;

hence contradiction by A7, A17, XCMPLX_1:6; :: thesis:

end;

A18: now

assume A19: ( r1 <> 0 & r2 <> 0 & s1 = 0 ) ; :: thesis:
then A20: s2 = 0 by A7, XCMPLX_1:6;
A21: v - u = (r1 * p) + (0. V) by A3, A19, RLVECT_1:23
.= r1 * p by RLVECT_1:10 ;
A22: y - w = (r2 * p) + (0. V) by A4, A20, RLVECT_1:23
.= r2 * p by RLVECT_1:10 ;
A23: (r1 " ) * (v - u) = ((r1 " ) * r1) * p by A21, RLVECT_1:def 9
.= 1 * p by A19, XCMPLX_0:def 7
.= p by RLVECT_1:def 9 ;
(r2 " ) * (y - w) = ((r2 " ) * r2) * p by A22, RLVECT_1:def 9
.= 1 * p by A19, XCMPLX_0:def 7
.= p by RLVECT_1:def 9 ;
then ( (r1 " ) * (v - u) = (r2 " ) * (y - w) & r1 " <> 0 & r2 " <> 0 ) by A19, A23, XCMPLX_1:203;
hence contradiction by A2, Lm1; :: thesis:

end;

now

assume A24: ( r1 <> 0 & r2 <> 0 & s1 <> 0 & s2 <> 0 ) ; :: thesis:
r2 * (v - u) = (r2 * (r1 * p)) + (r2 * (s1 * q)) by A3, RLVECT_1:def 9
.= ((r2 * r1) * p) + (r2 * (s1 * q)) by RLVECT_1:def 9
.= ((r1 * r2) * p) + ((r1 * s2) * q) by A7, RLVECT_1:def 9
.= (r1 * (r2 * p)) + ((r1 * s2) * q) by RLVECT_1:def 9
.= (r1 * (r2 * p)) + (r1 * (s2 * q)) by RLVECT_1:def 9
.= r1 * (y - w) by A4, RLVECT_1:def 9 ;
hence contradiction by A2, A24, Lm1; :: thesis:

end;

hence contradiction by A7, A8, A16, A18, XCMPLX_1:6; :: thesis:

end;

set a = (r2 * s3) - (r3 * s2);
set b = (r1 * s3) - (r3 * s1);
A25: ((r1 * s3) - (r3 * s1)) * r2 = (r1 * ((r2 * s3) - (r3 * s2))) + (r3 * ((r1 * s2) - (r2 * s1))) ;
A26: ((r1 * s3) - (r3 * s1)) * s2 = (s1 * ((r2 * s3) - (r3 * s2))) + (s3 * ((r1 * s2) - (r2 * s1))) ;

A27: now

assume ( (r2 * s3) - (r3 * s2) = 0 & (r1 * s3) - (r3 * s1) = 0 ) ; :: thesis:
then ( r3 = 0 & s3 = 0 ) by A6, A25, A26, XCMPLX_1:6;
then (0. V) + (0 * q) = u - w by A5, RLVECT_1:23;
then (0. V) + (0. V) = u - w by RLVECT_1:23;
then 0. V = u - w by RLVECT_1:10;
then u = w by RLVECT_1:35;
then ( u,v // u,u & w,y // w,u ) by Def1;
hence ex z being VECTOR of V st
( ( u,v // u,z or u,v // z,u ) & ( w,y // w,z or w,y // z,w ) ) ; :: thesis:

end;

set z = u + (((((r1 * s2) - (r2 * s1)) " ) * ((r2 * s3) - (r3 * s2))) * (v - u));
A28: ((r1 * s2) - (r2 * s1)) * ((u + (((((r1 * s2) - (r2 * s1)) " ) * ((r2 * s3) - (r3 * s2))) * (v - u))) - u) = (((r1 * s2) - (r2 * s1)) * (u + (((((r1 * s2) - (r2 * s1)) " ) * ((r2 * s3) - (r3 * s2))) * (v - u)))) - (((r1 * s2) - (r2 * s1)) * u) by RLVECT_1:48
.= ((((r1 * s2) - (r2 * s1)) * u) + (((r1 * s2) - (r2 * s1)) * (((((r1 * s2) - (r2 * s1)) " ) * ((r2 * s3) - (r3 * s2))) * (v - u)))) - (((r1 * s2) - (r2 * s1)) * u) by RLVECT_1:def 9
.= ((((r1 * s2) - (r2 * s1)) * u) + ((((r1 * s2) - (r2 * s1)) * ((((r1 * s2) - (r2 * s1)) " ) * ((r2 * s3) - (r3 * s2)))) * (v - u))) - (((r1 * s2) - (r2 * s1)) * u) by RLVECT_1:def 9
.= ((((r1 * s2) - (r2 * s1)) * u) + (((((r1 * s2) - (r2 * s1)) * (((r1 * s2) - (r2 * s1)) " )) * ((r2 * s3) - (r3 * s2))) * (v - u))) - (((r1 * s2) - (r2 * s1)) * u)
.= ((((r1 * s2) - (r2 * s1)) * u) + ((1 * ((r2 * s3) - (r3 * s2))) * (v - u))) - (((r1 * s2) - (r2 * s1)) * u) by A6, XCMPLX_0:def 7
.= (((r2 * s3) - (r3 * s2)) * (v - u)) + ((((r1 * s2) - (r2 * s1)) * u) - (((r1 * s2) - (r2 * s1)) * u)) by RLVECT_1:def 6
.= (((r2 * s3) - (r3 * s2)) * (v - u)) + (0. V) by RLVECT_1:28
.= ((r2 * s3) - (r3 * s2)) * (v - u) by RLVECT_1:10 ;
A29: ((r1 * s2) - (r2 * s1)) * ((u + (((((r1 * s2) - (r2 * s1)) " ) * ((r2 * s3) - (r3 * s2))) * (v - u))) - w) = (((r1 * s2) - (r2 * s1)) * (u + (((((r1 * s2) - (r2 * s1)) " ) * ((r2 * s3) - (r3 * s2))) * (v - u)))) - (((r1 * s2) - (r2 * s1)) * w) by RLVECT_1:48
.= ((((r1 * s2) - (r2 * s1)) * u) + (((r1 * s2) - (r2 * s1)) * (((((r1 * s2) - (r2 * s1)) " ) * ((r2 * s3) - (r3 * s2))) * (v - u)))) - (((r1 * s2) - (r2 * s1)) * w) by RLVECT_1:def 9
.= ((((r1 * s2) - (r2 * s1)) * u) + ((((r1 * s2) - (r2 * s1)) * ((((r1 * s2) - (r2 * s1)) " ) * ((r2 * s3) - (r3 * s2)))) * (v - u))) - (((r1 * s2) - (r2 * s1)) * w) by RLVECT_1:def 9
.= ((((r1 * s2) - (r2 * s1)) * u) + (((((r1 * s2) - (r2 * s1)) * (((r1 * s2) - (r2 * s1)) " )) * ((r2 * s3) - (r3 * s2))) * (v - u))) - (((r1 * s2) - (r2 * s1)) * w)
.= ((((r1 * s2) - (r2 * s1)) * u) + ((1 * ((r2 * s3) - (r3 * s2))) * (v - u))) - (((r1 * s2) - (r2 * s1)) * w) by A6, XCMPLX_0:def 7
.= (((r2 * s3) - (r3 * s2)) * (v - u)) + ((((r1 * s2) - (r2 * s1)) * u) - (((r1 * s2) - (r2 * s1)) * w)) by RLVECT_1:def 6
.= (((r2 * s3) - (r3 * s2)) * ((r1 * p) + (s1 * q))) + (((r1 * s2) - (r2 * s1)) * ((r3 * p) + (s3 * q))) by A3, A5, RLVECT_1:48
.= ((((r2 * s3) - (r3 * s2)) * (r1 * p)) + (((r2 * s3) - (r3 * s2)) * (s1 * q))) + (((r1 * s2) - (r2 * s1)) * ((r3 * p) + (s3 * q))) by RLVECT_1:def 9
.= ((((r2 * s3) - (r3 * s2)) * (r1 * p)) + (((r2 * s3) - (r3 * s2)) * (s1 * q))) + ((((r1 * s2) - (r2 * s1)) * (r3 * p)) + (((r1 * s2) - (r2 * s1)) * (s3 * q))) by RLVECT_1:def 9
.= (((((r2 * s3) - (r3 * s2)) * r1) * p) + (((r2 * s3) - (r3 * s2)) * (s1 * q))) + ((((r1 * s2) - (r2 * s1)) * (r3 * p)) + (((r1 * s2) - (r2 * s1)) * (s3 * q))) by RLVECT_1:def 9
.= (((((r2 * s3) - (r3 * s2)) * r1) * p) + ((((r2 * s3) - (r3 * s2)) * s1) * q)) + ((((r1 * s2) - (r2 * s1)) * (r3 * p)) + (((r1 * s2) - (r2 * s1)) * (s3 * q))) by RLVECT_1:def 9
.= (((((r2 * s3) - (r3 * s2)) * r1) * p) + ((((r2 * s3) - (r3 * s2)) * s1) * q)) + (((((r1 * s2) - (r2 * s1)) * r3) * p) + (((r1 * s2) - (r2 * s1)) * (s3 * q))) by RLVECT_1:def 9
.= (((((r2 * s3) - (r3 * s2)) * r1) * p) + ((((r2 * s3) - (r3 * s2)) * s1) * q)) + (((((r1 * s2) - (r2 * s1)) * s3) * q) + ((((r1 * s2) - (r2 * s1)) * r3) * p)) by RLVECT_1:def 9
.= ((((((r2 * s3) - (r3 * s2)) * r1) * p) + ((((r2 * s3) - (r3 * s2)) * s1) * q)) + ((((r1 * s2) - (r2 * s1)) * s3) * q)) + ((((r1 * s2) - (r2 * s1)) * r3) * p) by RLVECT_1:def 6
.= ((((((r2 * s3) - (r3 * s2)) * s1) * q) + ((((r1 * s2) - (r2 * s1)) * s3) * q)) + ((((r2 * s3) - (r3 * s2)) * r1) * p)) + ((((r1 * s2) - (r2 * s1)) * r3) * p) by RLVECT_1:def 6
.= (((((r2 * s3) - (r3 * s2)) * s1) * q) + ((((r1 * s2) - (r2 * s1)) * s3) * q)) + (((((r2 * s3) - (r3 * s2)) * r1) * p) + ((((r1 * s2) - (r2 * s1)) * r3) * p)) by RLVECT_1:def 6
.= (((((r2 * s3) - (r3 * s2)) * s1) + (((r1 * s2) - (r2 * s1)) * s3)) * q) + (((((r2 * s3) - (r3 * s2)) * r1) * p) + ((((r1 * s2) - (r2 * s1)) * r3) * p)) by RLVECT_1:def 9
.= ((((r1 * s3) - (r3 * s1)) * s2) * q) + ((((r1 * s3) - (r3 * s1)) * r2) * p) by A25, RLVECT_1:def 9
.= (((r1 * s3) - (r3 * s1)) * (s2 * q)) + ((((r1 * s3) - (r3 * s1)) * r2) * p) by RLVECT_1:def 9
.= (((r1 * s3) - (r3 * s1)) * (s2 * q)) + (((r1 * s3) - (r3 * s1)) * (r2 * p)) by RLVECT_1:def 9
.= ((r1 * s3) - (r3 * s1)) * (y - w) by A4, RLVECT_1:def 9 ;

A30: now

assume A31: ( (r2 * s3) - (r3 * s2) = 0 & (r1 * s3) - (r3 * s1) <> 0 ) ; :: thesis:
then ((r1 * s2) - (r2 * s1)) * ((u + (((((r1 * s2) - (r2 * s1)) " ) * ((r2 * s3) - (r3 * s2))) * (v - u))) - u) = 0. V by A28, RLVECT_1:23;
then (u + (((((r1 * s2) - (r2 * s1)) " ) * ((r2 * s3) - (r3 * s2))) * (v - u))) - u = 0. V by A6, RLVECT_1:24;
then u + (((((r1 * s2) - (r2 * s1)) " ) * ((r2 * s3) - (r3 * s2))) * (v - u)) = u by RLVECT_1:35;
then ( u,v // u,u + (((((r1 * s2) - (r2 * s1)) " ) * ((r2 * s3) - (r3 * s2))) * (v - u)) & ( w,y // w,u + (((((r1 * s2) - (r2 * s1)) " ) * ((r2 * s3) - (r3 * s2))) * (v - u)) or w,y // u + (((((r1 * s2) - (r2 * s1)) " ) * ((r2 * s3) - (r3 * s2))) * (v - u)),w ) ) by A29, A31, Def1, Lm1;
hence ex z being VECTOR of V st
( ( u,v // u,z or u,v // z,u ) & ( w,y // w,z or w,y // z,w ) ) ; :: thesis:

end;

A32: now

assume A33: ( (r2 * s3) - (r3 * s2) <> 0 & (r1 * s3) - (r3 * s1) = 0 ) ; :: thesis:
then ((r1 * s2) - (r2 * s1)) * ((u + (((((r1 * s2) - (r2 * s1)) " ) * ((r2 * s3) - (r3 * s2))) * (v - u))) - w) = 0. V by A29, RLVECT_1:23;
then (u + (((((r1 * s2) - (r2 * s1)) " ) * ((r2 * s3) - (r3 * s2))) * (v - u))) - w = 0. V by A6, RLVECT_1:24;
then u + (((((r1 * s2) - (r2 * s1)) " ) * ((r2 * s3) - (r3 * s2))) * (v - u)) = w by RLVECT_1:35;
then ( ( u,v // u,u + (((((r1 * s2) - (r2 * s1)) " ) * ((r2 * s3) - (r3 * s2))) * (v - u)) or u,v // u + (((((r1 * s2) - (r2 * s1)) " ) * ((r2 * s3) - (r3 * s2))) * (v - u)),u ) & w,y // w,u + (((((r1 * s2) - (r2 * s1)) " ) * ((r2 * s3) - (r3 * s2))) * (v - u)) ) by A28, A33, Def1, Lm1;
hence ex z being VECTOR of V st
( ( u,v // u,z or u,v // z,u ) & ( w,y // w,z or w,y // z,w ) ) ; :: thesis:

end;

now

assume ( (r2 * s3) - (r3 * s2) <> 0 & (r1 * s3) - (r3 * s1) <> 0 ) ; :: thesis:
then ( ( u,v // u,u + (((((r1 * s2) - (r2 * s1)) " ) * ((r2 * s3) - (r3 * s2))) * (v - u)) or u,v // u + (((((r1 * s2) - (r2 * s1)) " ) * ((r2 * s3) - (r3 * s2))) * (v - u)),u ) & ( w,y // w,u + (((((r1 * s2) - (r2 * s1)) " ) * ((r2 * s3) - (r3 * s2))) * (v - u)) or w,y // u + (((((r1 * s2) - (r2 * s1)) " ) * ((r2 * s3) - (r3 * s2))) * (v - u)),w ) ) by A28, A29, Lm1;
hence ex z being VECTOR of V st
( ( u,v // u,z or u,v // z,u ) & ( w,y // w,z or w,y // z,w ) ) ; :: thesis:

end;

hence ex z being VECTOR of V st
( ( u,v // u,z or u,v // z,u ) & ( w,y // w,z or w,y // z,w ) ) by A27, A30, A32; :: thesis: