let V be RealLinearSpace; :: thesis: ( ex u, v being VECTOR of V st

for a, b being Real st (a * u) + (b * v) = 0. V holds

( a = 0 & b = 0 ) implies ex u, v, w, y being VECTOR of V st

( not u,v // w,y & not u,v // y,w ) )

given u, v being VECTOR of V such that A1: for a, b being Real st (a * u) + (b * v) = 0. V holds

( a = 0 & b = 0 ) ; :: thesis: ex u, v, w, y being VECTOR of V st

( not u,v // w,y & not u,v // y,w )

A2: ( u <> 0. V & v <> 0. V ) by A1, Th19;

A3: not 0. V,u // v, 0. V

( not u,v // w,y & not u,v // y,w ) by A3; :: thesis: verum

for a, b being Real st (a * u) + (b * v) = 0. V holds

( a = 0 & b = 0 ) implies ex u, v, w, y being VECTOR of V st

( not u,v // w,y & not u,v // y,w ) )

given u, v being VECTOR of V such that A1: for a, b being Real st (a * u) + (b * v) = 0. V holds

( a = 0 & b = 0 ) ; :: thesis: ex u, v, w, y being VECTOR of V st

( not u,v // w,y & not u,v // y,w )

A2: ( u <> 0. V & v <> 0. V ) by A1, Th19;

A3: not 0. V,u // v, 0. V

proof

hence contradiction by A2, A4; :: thesis: verum

end;

not 0. V,u // 0. V,v
A4: now :: thesis: for a, b being Real holds

( not 0 < a or not 0 < b or not a * (u - (0. V)) = b * ((0. V) - v) )

assume
0. V,u // v, 0. V
; :: thesis: contradiction( not 0 < a or not 0 < b or not a * (u - (0. V)) = b * ((0. V) - v) )

given a, b being Real such that A5:
0 < a
and

0 < b and

A6: a * (u - (0. V)) = b * ((0. V) - v) ; :: thesis: contradiction

( a * u = a * (u - (0. V)) & b * ((0. V) - v) = b * (- v) ) by RLVECT_1:13, RLVECT_1:14;

then a * u = - (b * v) by A6, RLVECT_1:25;

then (a * u) + (b * v) = 0. V by RLVECT_1:5;

hence contradiction by A1, A5; :: thesis: verum

end;0 < b and

A6: a * (u - (0. V)) = b * ((0. V) - v) ; :: thesis: contradiction

( a * u = a * (u - (0. V)) & b * ((0. V) - v) = b * (- v) ) by RLVECT_1:13, RLVECT_1:14;

then a * u = - (b * v) by A6, RLVECT_1:25;

then (a * u) + (b * v) = 0. V by RLVECT_1:5;

hence contradiction by A1, A5; :: thesis: verum

hence contradiction by A2, A4; :: thesis: verum

proof

hence contradiction by A2, A7; :: thesis: verum

end;

hence
ex u, v, w, y being VECTOR of V st A7: now :: thesis: for a, b being Real holds

( not 0 < a or not 0 < b or not a * (u - (0. V)) = b * (v - (0. V)) )

assume
0. V,u // 0. V,v
; :: thesis: contradiction( not 0 < a or not 0 < b or not a * (u - (0. V)) = b * (v - (0. V)) )

given a, b being Real such that A8:
0 < a
and

0 < b and

A9: a * (u - (0. V)) = b * (v - (0. V)) ; :: thesis: contradiction

( a * u = a * (u - (0. V)) & b * (v - (0. V)) = b * v ) by RLVECT_1:13;

then 0. V = (a * u) - (b * v) by A9, RLVECT_1:15

.= (a * u) + (b * (- v)) by RLVECT_1:25

.= (a * u) + ((- b) * v) by RLVECT_1:24 ;

hence contradiction by A1, A8; :: thesis: verum

end;0 < b and

A9: a * (u - (0. V)) = b * (v - (0. V)) ; :: thesis: contradiction

( a * u = a * (u - (0. V)) & b * (v - (0. V)) = b * v ) by RLVECT_1:13;

then 0. V = (a * u) - (b * v) by A9, RLVECT_1:15

.= (a * u) + (b * (- v)) by RLVECT_1:25

.= (a * u) + ((- b) * v) by RLVECT_1:24 ;

hence contradiction by A1, A8; :: thesis: verum

hence contradiction by A2, A7; :: thesis: verum

( not u,v // w,y & not u,v // y,w ) by A3; :: thesis: verum