let V be RealLinearSpace; :: thesis: for p, q, r, u, v, w, y 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 p, q, r, u, v, w, y 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 and
A2: w,y,q are_LinDep and
A3: u,w,p are_LinDep and
A4: v,y,p are_LinDep and
A5: u,y,r are_LinDep and
A6: v,w,r are_LinDep and
A7: p,q,r are_LinDep and
A8: not p is zero and
A9: not q is zero and
A10: 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 A11: ( 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 A12: not v is zero by Th12;
A13: not w is zero by ;
A14: not y is zero by ;
A15: not u is zero by ;
not are_Prop v,y by ;
then consider a19, b19 being Real such that
A16: p = (a19 * v) + (b19 * y) by A4, A12, A14, Th6;
not are_Prop u,v by ;
then consider a2, b2 being Real such that
A17: q = (a2 * u) + (b2 * v) by A1, A15, A12, Th6;
not are_Prop v,w by ;
then consider a39, b39 being Real such that
A18: r = (a39 * v) + (b39 * w) by A6, A12, A13, Th6;
not are_Prop u,w by ;
then consider a1, b1 being Real such that
A19: p = (a1 * u) + (b1 * w) by A3, A15, A13, Th6;
not are_Prop w,y by ;
then consider a29, b29 being Real such that
A20: q = (a29 * w) + (b29 * y) by A2, A13, A14, Th6;
not are_Prop y,u by ;
then consider a3, b3 being Real such that
A21: r = (a3 * u) + (b3 * y) by A5, A15, A14, Th6;
consider A, B, C being Real such that
A22: ((A * p) + (B * q)) + (C * r) = 0. V and
A23: ( A <> 0 or B <> 0 or C <> 0 ) by A7;
A24: 0. V = ((((A * a1) + (C * a3)) * u) + (((A * b1) + (B * a29)) * w)) + (((B * b29) + (C * b3)) * y) by A19, A20, A21, A22, Lm9;
then A25: (A * a1) + (C * a3) = 0 by A11;
A26: 0. V = ((C * ((a39 * v) + (b39 * w))) + (B * ((a29 * w) + (b29 * y)))) + (A * ((a19 * v) + (b19 * y))) by
.= ((((C * a39) + (A * a19)) * v) + (((C * b39) + (B * a29)) * w)) + (((B * b29) + (A * b19)) * y) by Lm9 ;
then A27: (C * a39) + (A * a19) = 0 by A11;
A28: 0. V = ((((B * a2) + (C * a3)) * u) + (((B * b2) + (A * a19)) * v)) + (((A * b19) + (C * b3)) * y) by A16, A17, A21, A22, Lm9;
then A29: (B * a2) + (C * a3) = 0 by A11;
A30: 0. V = ((((B * a2) + (A * a1)) * u) + (((B * b2) + (C * a39)) * v)) + (((C * b39) + (A * b1)) * w) by A19, A17, A18, A22, Lm9;
then A31: (B * a2) + (A * a1) = 0 by A11;
A32: (C * b39) + (B * a29) = 0 by ;
A33: (C * b39) + (A * b1) = 0 by ;
A34: (B * b29) + (A * b19) = 0 by ;
A35: (A * b19) + (C * b3) = 0 by ;
A36: (B * b29) + (C * b3) = 0 by ;
A37: now :: thesis: not C <> 0
assume A38: C <> 0 ; :: thesis: contradiction
then a3 = 0 by ;
then r = (0 * u) + (0 * y) by
.= (0. V) + (0 * y) by RLVECT_1:10
.= (0. V) + (0. V) by RLVECT_1:10
.= 0. V ;
hence contradiction by A10; :: thesis: verum
end;
A39: (B * b2) + (C * a39) = 0 by ;
A40: (B * b2) + (A * a19) = 0 by ;
A41: now :: thesis: not B <> 0
assume A42: B <> 0 ; :: thesis: contradiction
then a2 = 0 by ;
then q = (0 * u) + (0 * v) by
.= (0. V) + (0 * v) by RLVECT_1:10
.= (0. V) + (0. V) by RLVECT_1:10
.= 0. V ;
hence contradiction by A9; :: thesis: verum
end;
A43: (A * b1) + (B * a29) = 0 by ;
now :: thesis: not A <> 0
assume A44: A <> 0 ; :: thesis: contradiction
then a1 = 0 by ;
then p = (0 * u) + (0 * w) by
.= (0. V) + (0 * w) by RLVECT_1:10
.= (0. V) + (0. V) by RLVECT_1:10
.= 0. V ;
hence contradiction by A8; :: thesis: verum
end;
hence contradiction by A23, A41, A37; :: thesis: verum