let V be RealLinearSpace; :: thesis: for o, u, u2 being Element of V st o,u,u2 are_LinDep & not are_Prop o,u & not are_Prop o,u2 & not are_Prop u,u2 & o,u,u2 are_Prop_Vect holds
( ex a1, b1 being Real st
( b1 * u2 = o + (a1 * u) & a1 <> 0 & b1 <> 0 ) & ex a2, c2 being Real st
( u2 = (c2 * o) + (a2 * u) & c2 <> 0 & a2 <> 0 ) )
let o, u, u2 be Element of V; :: thesis: ( o,u,u2 are_LinDep & not are_Prop o,u & not are_Prop o,u2 & not are_Prop u,u2 & o,u,u2 are_Prop_Vect implies ( ex a1, b1 being Real st
( b1 * u2 = o + (a1 * u) & a1 <> 0 & b1 <> 0 ) & ex a2, c2 being Real st
( u2 = (c2 * o) + (a2 * u) & c2 <> 0 & a2 <> 0 ) ) )
assume A1: ( o,u,u2 are_LinDep & not are_Prop o,u & not are_Prop o,u2 & not are_Prop u,u2 & o,u,u2 are_Prop_Vect ) ; :: thesis: ( ex a1, b1 being Real st
( b1 * u2 = o + (a1 * u) & a1 <> 0 & b1 <> 0 ) & ex a2, c2 being Real st
( u2 = (c2 * o) + (a2 * u) & c2 <> 0 & a2 <> 0 ) )
then consider a, b, c being Real such that
A2: ( ((a * o) + (b * u)) + (c * u2) = 0. V & ( a <> 0 or b <> 0 or c <> 0 ) ) by ANPROJ_1:def 3;
( not o is zero & not u is zero & not u2 is zero ) by A1, Def1;
then A3: ( o <> 0. V & u <> 0. V & u2 <> 0. V ) by STRUCT_0:def 15;
A4: ( a <> 0 & b <> 0 & c <> 0 )

proof

assume A5: ( not a <> 0 or not b <> 0 or not c <> 0 ) ; :: thesis: contradiction

A6: now

assume A7: a = 0 ; :: thesis: contradiction
A8: ( b <> 0 & c <> 0 )

proof

assume A9: ( not b <> 0 or not c <> 0 ) ; :: thesis: contradiction

A10: now

assume A11: b = 0 ; :: thesis: contradiction
then 0. V = ((0. V) + (0 * u)) + (c * u2) by A2, A7, 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 A2, A3, A7, A11, RLVECT_1:24; :: thesis: verum

end;

now

assume A12: c = 0 ; :: thesis: contradiction
then 0. V = ((0. V) + (b * u)) + (0 * u2) by A2, A7, 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 A2, A3, A7, A12, RLVECT_1:24; :: thesis: verum

end;

hence contradiction by A9, A10; :: thesis: verum

end;

0. V = ((0. V) + (b * u)) + (c * u2) by A2, A7, 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 A13: b * u = (- c) * u2 by RLVECT_1:38;
- c <> 0 by A8;
hence contradiction by A1, A8, A13, ANPROJ_1:def 2; :: thesis: verum

end;

A14: now

assume A15: b = 0 ; :: thesis: contradiction
A16: ( a <> 0 & c <> 0 )

proof

assume A17: ( not a <> 0 or not c <> 0 ) ; :: thesis: contradiction

A18: now

assume A19: a = 0 ; :: thesis: contradiction
then 0. V = ((0. V) + (0 * u)) + (c * u2) by A2, A15, 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 A2, A3, A15, A19, RLVECT_1:24; :: thesis: verum

end;

now

assume A20: c = 0 ; :: thesis: contradiction
then 0. V = ((a * o) + (0 * u)) + (0. V) by A2, A15, 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 A2, A3, A15, A20, RLVECT_1:24; :: thesis: verum

end;

hence contradiction by A17, A18; :: thesis: verum

end;

0. V = ((a * o) + (0. V)) + (c * u2) by A2, A15, 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 A21: a * o = (- c) * u2 by RLVECT_1:38;
- c <> 0 by A16;
hence contradiction by A1, A16, A21, ANPROJ_1:def 2; :: thesis: verum

end;

now

assume A22: c = 0 ; :: thesis: contradiction
A23: ( a <> 0 & b <> 0 )

proof

assume A24: ( not a <> 0 or not b <> 0 ) ; :: thesis: contradiction

A25: now

assume A26: a = 0 ; :: thesis: contradiction
then 0. V = ((0. V) + (b * u)) + (0 * u2) by A2, A22, 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 A2, A3, A22, A26, RLVECT_1:24; :: thesis: verum

end;

now

assume A27: b = 0 ; :: thesis: contradiction
then 0. V = ((a * o) + (0 * u)) + (0. V) by A2, A22, 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 A2, A3, A22, A27, RLVECT_1:24; :: thesis: verum

end;

hence contradiction by A24, A25; :: thesis: verum

end;

0. V = ((a * o) + (b * u)) + (0. V) by A2, A22, 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 A28: a * o = (- b) * u by RLVECT_1:38;
- b <> 0 by A23;
hence contradiction by A1, A23, A28, ANPROJ_1:def 2; :: thesis: verum

end;

hence contradiction by A5, A6, A14; :: thesis: verum

end;

(a " ) * (- (c * u2)) = (a " ) * ((a * o) + (b * u)) by A2, 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 A4, XCMPLX_0:def 7
.= o + (((a " ) * b) * u) by RLVECT_1:def 9 ;
then A29: 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 ;
A30: ( a " <> 0 & c " <> 0 ) by A4, XCMPLX_1:203;
then A31: (a " ) * b <> 0 by A4, XCMPLX_1:6;
- ((a " ) * c) <> 0 by A4, A30, XCMPLX_1:6;
hence ex a1, b1 being Real st
( b1 * u2 = o + (a1 * u) & a1 <> 0 & b1 <> 0 ) by A29, A31; :: thesis: ex a2, c2 being Real st
( u2 = (c2 * o) + (a2 * u) & c2 <> 0 & a2 <> 0 )
c * u2 = - ((a * o) + (b * u)) by A2, 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 A32: (((c " ) * (- a)) * o) + (((c " ) * (- b)) * u) = ((c " ) * c) * u2 by RLVECT_1:def 9
.= 1 * u2 by A4, XCMPLX_0:def 7
.= u2 by RLVECT_1:def 9 ;
A33: (c " ) * (- a) <> 0

proof

- a <> 0 by A4;
hence (c " ) * (- a) <> 0 by A30, XCMPLX_1:6; :: thesis: verum

end;

(c " ) * (- b) <> 0

proof

- b <> 0 by A4;
hence (c " ) * (- b) <> 0 by A30, XCMPLX_1:6; :: thesis: verum

end;

hence ex a2, c2 being Real st
( u2 = (c2 * o) + (a2 * u) & c2 <> 0 & a2 <> 0 ) by A32, A33; :: thesis: verum