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, ANPROJ_1:def 3;
not u is zero by A5, Def1;
then A8: u <> 0. V by STRUCT_0:def 12;
not u2 is zero by A5, Def1;
then A9: u2 <> 0. V by STRUCT_0:def 12;
not o is zero by A5, Def1;
then A10: o <> 0. V by STRUCT_0:def 12;
A11: ( a <> 0 & b <> 0 & c <> 0 )

proof

A12: now

assume A13: b = 0 ; :: thesis:
then 0. V = ((a * o) + (0. V)) + (c * u2) by A6, RLVECT_1:23
.= (a * o) + (c * u2) by RLVECT_1:10 ;
then a * o = - (c * u2) by RLVECT_1:19
.= c * (- u2) by RLVECT_1:39 ;
then A14: a * o = (- c) * u2 by RLVECT_1:38;
A15: ( a <> 0 & c <> 0 )

proof

A16: now

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

end;

A18: now

assume A19: a = 0 ; :: thesis:
then 0. V = ((0. V) + (0 * u)) + (c * u2) by A6, A13, RLVECT_1:23
.= (0 * u) + (c * u2) by RLVECT_1:10
.= (0. V) + (c * u2) by RLVECT_1:23
.= c * u2 by RLVECT_1:10 ;
hence contradiction by A7, A9, A13, A19, RLVECT_1:24; :: 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, ANPROJ_1:def 2; :: thesis:

end;

A20: now

assume A21: a = 0 ; :: thesis:
then 0. V = ((0. V) + (b * u)) + (c * u2) by A6, RLVECT_1:23
.= (b * u) + (c * u2) by RLVECT_1:10 ;
then b * u = - (c * u2) by RLVECT_1:19
.= c * (- u2) by RLVECT_1:39 ;
then A22: b * u = (- c) * u2 by RLVECT_1:38;
A23: ( b <> 0 & c <> 0 )

proof

A24: now

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

end;

A26: now

assume A27: b = 0 ; :: thesis:
then 0. V = ((0. V) + (0 * u)) + (c * u2) by A6, A21, RLVECT_1:23
.= (0 * u) + (c * u2) by RLVECT_1:10
.= (0. V) + (c * u2) by RLVECT_1:23
.= c * u2 by RLVECT_1:10 ;
hence contradiction by A7, A9, A21, A27, RLVECT_1:24; :: 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, ANPROJ_1:def 2; :: thesis:

end;

A28: now

assume A29: c = 0 ; :: thesis:
then 0. V = ((a * o) + (b * u)) + (0. V) by A6, RLVECT_1:23
.= (a * o) + (b * u) by RLVECT_1:10 ;
then a * o = - (b * u) by RLVECT_1:19
.= b * (- u) by RLVECT_1:39 ;
then A30: a * o = (- b) * u by RLVECT_1:38;
A31: ( a <> 0 & b <> 0 )

proof

A32: now

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

end;

A34: now

assume A35: a = 0 ; :: thesis:
then 0. V = ((0. V) + (b * u)) + (0 * u2) by A6, A29, RLVECT_1:23
.= (b * u) + (0 * u2) by RLVECT_1:10
.= (b * u) + (0. V) by RLVECT_1:23
.= b * u by RLVECT_1:10 ;
hence contradiction by A7, A8, A29, A35, RLVECT_1:24; :: 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, ANPROJ_1:def 2; :: 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:203;
a " <> 0 by A11, XCMPLX_1:203;
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:19
.= ((a " ) * (a * o)) + ((a " ) * (b * u)) by RLVECT_1:def 9
.= (((a " ) * a) * o) + ((a " ) * (b * u)) by RLVECT_1:def 9
.= (((a " ) * a) * o) + (((a " ) * b) * u) by RLVECT_1:def 9
.= (1 * o) + (((a " ) * b) * u) by A11, XCMPLX_0:def 7
.= o + (((a " ) * b) * u) by RLVECT_1:def 9 ;
then o + (((a " ) * b) * u) = (a " ) * (c * (- u2)) by RLVECT_1:39
.= ((a " ) * c) * (- u2) by RLVECT_1:def 9
.= (- ((a " ) * c)) * u2 by RLVECT_1:38 ;
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 11
.= (- (a * o)) + (- (b * u)) by RLVECT_1:45
.= ((- 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 9
.= (((c " ) * (- a)) * o) + ((c " ) * ((- b) * u)) by RLVECT_1:def 9
.= (((c " ) * (- a)) * o) + (((c " ) * (- b)) * u) by RLVECT_1:def 9 ;
then A39: (((c " ) * (- a)) * o) + (((c " ) * (- b)) * u) = ((c " ) * c) * u2 by RLVECT_1:def 9
.= 1 * u2 by A11, XCMPLX_0:def 7
.= u2 by RLVECT_1:def 9 ;
- 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: