let V be RealLinearSpace; :: thesis:
let o, u, u2 be Element of V; :: thesis:
assume that
A1: o,u,u2 are_LinDep and
A2: not are_Prop o,u and
A3: not are_Prop o,u2 and
A4: not are_Prop u,u2 and
A5: o,u,u2 are_Prop_Vect ; :: thesis:
consider a, b, c being Real such that
A6: ((a * o) + (b * u)) + (c * u2) = 0. V and
A7: ( a <> 0 or b <> 0 or c <> 0 ) by A1;
not u is zero by A5;
then A8: u <> 0. V ;
not u2 is zero by A5;
then A9: u2 <> 0. V ;
not o is zero by A5;
then A10: o <> 0. V ;
A11: ( a <> 0 & b <> 0 & c <> 0 )

proof

A12: now :: thesis:

assume A13: b = 0 ; :: thesis:
then 0. V = ((a * o) + (0. V)) + (c * u2) by A6, RLVECT_1:10
.= (a * o) + (c * u2) by RLVECT_1:4 ;
then a * o = - (c * u2) by RLVECT_1:6
.= c * (- u2) by RLVECT_1:25 ;
then A14: a * o = (- c) * u2 by RLVECT_1:24;
A15: ( a <> 0 & c <> 0 )

proof

A16: now :: thesis:

assume A17: c = 0 ; :: thesis:
then 0. V = ((a * o) + (0 * u)) + (0. V) by A6, A13, RLVECT_1:10
.= (a * o) + (0 * u) by RLVECT_1:4
.= (a * o) + (0. V) by RLVECT_1:10
.= a * o by RLVECT_1:4 ;
hence contradiction by A7, A10, A13, A17, RLVECT_1:11; :: thesis:

end;

A18: now :: thesis:

assume A19: a = 0 ; :: thesis:
then 0. V = ((0. V) + (0 * u)) + (c * u2) by A6, A13, RLVECT_1:10
.= (0 * u) + (c * u2) by RLVECT_1:4
.= (0. V) + (c * u2) by RLVECT_1:10
.= c * u2 by RLVECT_1:4 ;
hence contradiction by A7, A9, A13, A19, RLVECT_1:11; :: thesis:

end;

assume ( not a <> 0 or not c <> 0 ) ; :: thesis:
hence contradiction by A18, A16; :: thesis:

end;

then - c <> 0 ;
hence contradiction by A3, A15, A14; :: thesis:

end;

A20: now :: thesis:

assume A21: a = 0 ; :: thesis:
then 0. V = ((0. V) + (b * u)) + (c * u2) by A6, RLVECT_1:10
.= (b * u) + (c * u2) by RLVECT_1:4 ;
then b * u = - (c * u2) by RLVECT_1:6
.= c * (- u2) by RLVECT_1:25 ;
then A22: b * u = (- c) * u2 by RLVECT_1:24;
A23: ( b <> 0 & c <> 0 )

proof

A24: now :: thesis:

assume A25: c = 0 ; :: thesis:
then 0. V = ((0. V) + (b * u)) + (0 * u2) by A6, A21, RLVECT_1:10
.= (b * u) + (0 * u2) by RLVECT_1:4
.= (b * u) + (0. V) by RLVECT_1:10
.= b * u by RLVECT_1:4 ;
hence contradiction by A7, A8, A21, A25, RLVECT_1:11; :: thesis:

end;

A26: now :: thesis:

assume A27: b = 0 ; :: thesis:
then 0. V = ((0. V) + (0 * u)) + (c * u2) by A6, A21, RLVECT_1:10
.= (0 * u) + (c * u2) by RLVECT_1:4
.= (0. V) + (c * u2) by RLVECT_1:10
.= c * u2 by RLVECT_1:4 ;
hence contradiction by A7, A9, A21, A27, RLVECT_1:11; :: thesis:

end;

assume ( not b <> 0 or not c <> 0 ) ; :: thesis:
hence contradiction by A26, A24; :: thesis:

end;

then - c <> 0 ;
hence contradiction by A4, A23, A22; :: thesis:

end;

A28: now :: thesis:

assume A29: c = 0 ; :: thesis:
then 0. V = ((a * o) + (b * u)) + (0. V) by A6, RLVECT_1:10
.= (a * o) + (b * u) by RLVECT_1:4 ;
then a * o = - (b * u) by RLVECT_1:6
.= b * (- u) by RLVECT_1:25 ;
then A30: a * o = (- b) * u by RLVECT_1:24;
A31: ( a <> 0 & b <> 0 )

proof

A32: now :: thesis:

assume A33: b = 0 ; :: thesis:
then 0. V = ((a * o) + (0 * u)) + (0. V) by A6, A29, RLVECT_1:10
.= (a * o) + (0 * u) by RLVECT_1:4
.= (a * o) + (0. V) by RLVECT_1:10
.= a * o by RLVECT_1:4 ;
hence contradiction by A7, A10, A29, A33, RLVECT_1:11; :: thesis:

end;

A34: now :: thesis:

assume A35: a = 0 ; :: thesis:
then 0. V = ((0. V) + (b * u)) + (0 * u2) by A6, A29, RLVECT_1:10
.= (b * u) + (0 * u2) by RLVECT_1:4
.= (b * u) + (0. V) by RLVECT_1:10
.= b * u by RLVECT_1:4 ;
hence contradiction by A7, A8, A29, A35, RLVECT_1:11; :: thesis:

end;

assume ( not a <> 0 or not b <> 0 ) ; :: thesis:
hence contradiction by A34, A32; :: thesis:

end;

then - b <> 0 ;
hence contradiction by A2, A31, A30; :: thesis:

end;

assume ( not a <> 0 or not b <> 0 or not c <> 0 ) ; :: thesis:
hence contradiction by A20, A12, A28; :: thesis:

end;

then A36: c " <> 0 by XCMPLX_1:202;
a " <> 0 by A11, XCMPLX_1:202;
then A37: ( (a ") * b <> 0 & - ((a ") * c) <> 0 ) by A11, XCMPLX_1:6;
(a ") * (- (c * u2)) = (a ") * ((a * o) + (b * u)) by A6, RLVECT_1:6
.= ((a ") * (a * o)) + ((a ") * (b * u)) by RLVECT_1:def 5
.= (((a ") * a) * o) + ((a ") * (b * u)) by RLVECT_1:def 7
.= (((a ") * a) * o) + (((a ") * b) * u) by RLVECT_1:def 7
.= (1 * o) + (((a ") * b) * u) by A11, XCMPLX_0:def 7
.= o + (((a ") * b) * u) by RLVECT_1:def 8 ;
then o + (((a ") * b) * u) = (a ") * (c * (- u2)) by RLVECT_1:25
.= ((a ") * c) * (- u2) by RLVECT_1:def 7
.= (- ((a ") * c)) * u2 by RLVECT_1:24 ;
hence ex a1, b1 being Real st
( b1 * u2 = o + (a1 * u) & a1 <> 0 & b1 <> 0 ) by A37; :: thesis:
- b <> 0 by A11;
then A38: (c ") * (- b) <> 0 by A36, XCMPLX_1:6;
c * u2 = - ((a * o) + (b * u)) by A6, RLVECT_1:def 10
.= (- (a * o)) + (- (b * u)) by RLVECT_1:31
.= ((- a) * o) + (- (b * u)) by Lm8
.= ((- a) * o) + ((- b) * u) by Lm8 ;
then (c ") * (c * u2) = ((c ") * ((- a) * o)) + ((c ") * ((- b) * u)) by RLVECT_1:def 5
.= (((c ") * (- a)) * o) + ((c ") * ((- b) * u)) by RLVECT_1:def 7
.= (((c ") * (- a)) * o) + (((c ") * (- b)) * u) by RLVECT_1:def 7 ;
then A39: (((c ") * (- a)) * o) + (((c ") * (- b)) * u) = ((c ") * c) * u2 by RLVECT_1:def 7
.= 1 * u2 by A11, XCMPLX_0:def 7
.= u2 by RLVECT_1:def 8 ;
- a <> 0 by A11;
then (c ") * (- a) <> 0 by A36, XCMPLX_1:6;
hence ex a2, c2 being Real st
( u2 = (c2 * o) + (a2 * u) & c2 <> 0 & a2 <> 0 ) by A39, A38; :: thesis: