let V be RealLinearSpace; :: thesis: for u, v, q, w, y, p, r being Element of V st u,v,q are_LinDep & w,y,q are_LinDep & u,w,p are_LinDep & v,y,p are_LinDep & u,y,r are_LinDep & v,w,r are_LinDep & p,q,r are_LinDep & not p is zero & not q is zero & not r is zero & not u,v,y are_LinDep & not u,v,w are_LinDep & not u,w,y are_LinDep holds
v,w,y are_LinDep
let u, v, q, w, y, p, r be Element of V; :: thesis: ( u,v,q are_LinDep & w,y,q are_LinDep & u,w,p are_LinDep & v,y,p are_LinDep & u,y,r are_LinDep & v,w,r are_LinDep & p,q,r are_LinDep & not p is zero & not q is zero & not r is zero & not u,v,y are_LinDep & not u,v,w are_LinDep & not u,w,y are_LinDep implies v,w,y are_LinDep )
assume that
A1: ( u,v,q are_LinDep & w,y,q are_LinDep & u,w,p are_LinDep & v,y,p are_LinDep & u,y,r are_LinDep & v,w,r are_LinDep ) and
A2: p,q,r are_LinDep and
A3: ( not p is zero & not q is zero & not r is zero ) ; :: thesis: ( u,v,y are_LinDep or u,v,w are_LinDep or u,w,y are_LinDep or v,w,y are_LinDep )
assume A4: ( not u,v,y are_LinDep & not u,v,w are_LinDep & not u,w,y are_LinDep & not v,w,y are_LinDep ) ; :: thesis: contradiction
then A5: ( not u is zero & not v is zero & not w is zero & not y is zero ) by Th17;
A6: ( not are_Prop u,v & not are_Prop v,y & not are_Prop y,u & not are_Prop v,w & not are_Prop w,y & not are_Prop u,w ) by A4, Th17;
then consider a1, b1 being Real such that
A7: p = (a1 * u) + (b1 * w) by A1, A5, Th11;
consider a1', b1' being Real such that
A8: p = (a1' * v) + (b1' * y) by A1, A5, A6, Th11;
consider a2, b2 being Real such that
A9: q = (a2 * u) + (b2 * v) by A1, A5, A6, Th11;
consider a2', b2' being Real such that
A10: q = (a2' * w) + (b2' * y) by A1, A5, A6, Th11;
consider a3, b3 being Real such that
A11: r = (a3 * u) + (b3 * y) by A1, A5, A6, Th11;
consider a3', b3' being Real such that
A12: r = (a3' * v) + (b3' * w) by A1, A5, A6, Th11;
consider A, B, C being Real such that
A13: ( ((A * p) + (B * q)) + (C * r) = 0. V & ( A <> 0 or B <> 0 or C <> 0 ) ) by A2, Def3;
0. V = ((((A * a1) + (C * a3)) * u) + (((A * b1) + (B * a2')) * w)) + (((B * b2') + (C * b3)) * y) by A7, A10, A11, A13, Lm9;
then A14: ( (A * a1) + (C * a3) = 0 & (A * b1) + (B * a2') = 0 & (B * b2') + (C * b3) = 0 ) by A4, Def3;
0. V = ((((B * a2) + (C * a3)) * u) + (((B * b2) + (A * a1')) * v)) + (((A * b1') + (C * b3)) * y) by A8, A9, A11, A13, Lm9;
then A15: ( (B * a2) + (C * a3) = 0 & (B * b2) + (A * a1') = 0 & (A * b1') + (C * b3) = 0 ) by A4, Def3;
0. V = ((((B * a2) + (A * a1)) * u) + (((B * b2) + (C * a3')) * v)) + (((C * b3') + (A * b1)) * w) by A7, A9, A12, A13, Lm9;
then A16: ( (B * a2) + (A * a1) = 0 & (B * b2) + (C * a3') = 0 & (C * b3') + (A * b1) = 0 ) by A4, Def3;
0. V = ((C * ((a3' * v) + (b3' * w))) + (B * ((a2' * w) + (b2' * y)))) + (A * ((a1' * v) + (b1' * y))) by A8, A10, A12, A13, RLVECT_1:def 6
.= ((((C * a3') + (A * a1')) * v) + (((C * b3') + (B * a2')) * w)) + (((B * b2') + (A * b1')) * y) by Lm9 ;
then A17: ( (C * a3') + (A * a1') = 0 & (C * b3') + (B * a2') = 0 & (B * b2') + (A * b1') = 0 ) by A4, Def3;

A18: now

assume A19: A <> 0 ; :: thesis: contradiction
then a1 = 0 by A14, A15, A16, XCMPLX_1:6;
then p = (0 * u) + (0 * w) by A7, A14, A16, A17, A19, XCMPLX_1:6
.= (0. V) + (0 * w) by RLVECT_1:23
.= (0. V) + (0. V) by RLVECT_1:23
.= 0. V by RLVECT_1:10 ;
hence contradiction by A3, STRUCT_0:def 15; :: thesis: verum

end;

A20: now

assume A21: B <> 0 ; :: thesis: contradiction
then a2 = 0 by A14, A15, A16, XCMPLX_1:6;
then q = (0 * u) + (0 * v) by A9, A15, A16, A17, A21, XCMPLX_1:6
.= (0. V) + (0 * v) by RLVECT_1:23
.= (0. V) + (0. V) by RLVECT_1:23
.= 0. V by RLVECT_1:10 ;
hence contradiction by A3, STRUCT_0:def 15; :: thesis: verum

end;

now

assume A22: C <> 0 ; :: thesis: contradiction
then a3 = 0 by A14, A15, A16, XCMPLX_1:6;
then r = (0 * u) + (0 * y) by A11, A14, A15, A17, A22, XCMPLX_1:6
.= (0. V) + (0 * y) by RLVECT_1:23
.= (0. V) + (0. V) by RLVECT_1:23
.= 0. V by RLVECT_1:10 ;
hence contradiction by A3, STRUCT_0:def 15; :: thesis: verum

end;

hence contradiction by A13, A18, A20; :: thesis: verum