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 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: ( 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 ) )

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: not b = 0
assume A13: b = 0 ; :: thesis: contradiction
then 0. V = ((a * o) + (0. V)) + (c * u2) by
.= (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: not c = 0
assume A17: c = 0 ; :: thesis: contradiction
then 0. V = ((a * o) + (0 * u)) + (0. V) by
.= (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: verum
end;
A18: now :: thesis: not a = 0
assume A19: a = 0 ; :: thesis: contradiction
then 0. V = ((0. V) + (0 * u)) + (c * u2) by
.= (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: verum
end;
assume ( not a <> 0 or not c <> 0 ) ; :: thesis: contradiction
hence contradiction by A18, A16; :: thesis: verum
end;
then - c <> 0 ;
hence contradiction by A3, A15, A14; :: thesis: verum
end;
A20: now :: thesis: not a = 0
assume A21: a = 0 ; :: thesis: contradiction
then 0. V = ((0. V) + (b * u)) + (c * u2) by
.= (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: not c = 0
assume A25: c = 0 ; :: thesis: contradiction
then 0. V = ((0. V) + (b * u)) + (0 * u2) by
.= (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: verum
end;
A26: now :: thesis: not b = 0
assume A27: b = 0 ; :: thesis: contradiction
then 0. V = ((0. V) + (0 * u)) + (c * u2) by
.= (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: verum
end;
assume ( not b <> 0 or not c <> 0 ) ; :: thesis: contradiction
hence contradiction by A26, A24; :: thesis: verum
end;
then - c <> 0 ;
hence contradiction by A4, A23, A22; :: thesis: verum
end;
A28: now :: thesis: not c = 0
assume A29: c = 0 ; :: thesis: contradiction
then 0. V = ((a * o) + (b * u)) + (0. V) by
.= (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: not b = 0
assume A33: b = 0 ; :: thesis: contradiction
then 0. V = ((a * o) + (0 * u)) + (0. V) by
.= (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: verum
end;
A34: now :: thesis: not a = 0
assume A35: a = 0 ; :: thesis: contradiction
then 0. V = ((0. V) + (b * u)) + (0 * u2) by
.= (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: verum
end;
assume ( not a <> 0 or not b <> 0 ) ; :: thesis: contradiction
hence contradiction by A34, A32; :: thesis: verum
end;
then - b <> 0 ;
hence contradiction by A2, A31, A30; :: thesis: verum
end;
assume ( not a <> 0 or not b <> 0 or not c <> 0 ) ; :: thesis: contradiction
hence contradiction by A20, A12, A28; :: thesis: verum
end;
then A36: c " <> 0 by XCMPLX_1:202;
a " <> 0 by ;
then A37: ( (a ") * b <> 0 & - ((a ") * c) <> 0 ) by ;
(a ") * (- (c * u2)) = (a ") * ((a * o) + (b * u)) by
.= ((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
.= 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: ex a2, c2 being Real st
( u2 = (c2 * o) + (a2 * u) & c2 <> 0 & a2 <> 0 )

- b <> 0 by A11;
then A38: (c ") * (- b) <> 0 by ;
c * u2 = - ((a * o) + (b * u)) by
.= (- (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
.= u2 by RLVECT_1:def 8 ;
- a <> 0 by A11;
then (c ") * (- a) <> 0 by ;
hence ex a2, c2 being Real st
( u2 = (c2 * o) + (a2 * u) & c2 <> 0 & a2 <> 0 ) by ; :: thesis: verum