let V be RealLinearSpace; :: thesis: for p, q, u, v, w being Element of V st not are_Prop p,q & p,q,u are_LinDep & p,q,v are_LinDep & p,q,w are_LinDep & not p is zero & not q is zero holds
u,v,w are_LinDep

let p, q, u, v, w be Element of V; :: thesis: ( not are_Prop p,q & p,q,u are_LinDep & p,q,v are_LinDep & p,q,w are_LinDep & not p is zero & not q is zero implies u,v,w are_LinDep )
assume that
A1: not are_Prop p,q and
A2: p,q,u are_LinDep and
A3: p,q,v are_LinDep and
A4: p,q,w are_LinDep and
A5: ( not p is zero & not q is zero ) ; :: thesis: u,v,w are_LinDep
consider a1, b1 being Real such that
A6: u = (a1 * p) + (b1 * q) by A1, A2, A5, Th6;
consider a3, b3 being Real such that
A7: w = (a3 * p) + (b3 * q) by A1, A4, A5, Th6;
consider a2, b2 being Real such that
A8: v = (a2 * p) + (b2 * q) by A1, A3, A5, Th6;
set a = (a2 * b3) - (a3 * b2);
set b = (- (a1 * b3)) + (a3 * b1);
set c = (a1 * b2) - (a2 * b1);
A9: now :: thesis: ( (a2 * b3) - (a3 * b2) = 0 & (- (a1 * b3)) + (a3 * b1) = 0 & (a1 * b2) - (a2 * b1) = 0 implies u,v,w are_LinDep )
A10: ( w = 0. V & v = 0. V & ( are_Prop v,w or v = 0. V or w = 0. V ) implies u,v,w are_LinDep ) by Th10;
A11: ( w = 0. V & u = 0. V & ( are_Prop v,w or v = 0. V or w = 0. V ) implies u,v,w are_LinDep ) by Th10;
A12: ( u = 0. V & v = 0. V & ( are_Prop v,w or v = 0. V or w = 0. V ) implies u,v,w are_LinDep ) by Th10;
A13: ( ( ( w = 0. V & are_Prop u,v & w = 0. V ) or ( u = 0. V & u = 0. V & are_Prop v,w ) or ( are_Prop w,u & v = 0. V & v = 0. V ) ) implies u,v,w are_LinDep ) by Th11;
A14: ( are_Prop w,u & are_Prop u,v & are_Prop v,w implies u,v,w are_LinDep ) by Th11;
assume that
A15: (a2 * b3) - (a3 * b2) = 0 and
A16: (- (a1 * b3)) + (a3 * b1) = 0 and
A17: (a1 * b2) - (a2 * b1) = 0 ; :: thesis: u,v,w are_LinDep
0 = (a3 * b1) - (a1 * b3) by A16;
hence u,v,w are_LinDep by A1, A5, A6, A8, A7, A15, A17, A14, A13, A11, A10, A12, Th9; :: thesis: verum
end;
( 0. V = (((((a2 * b3) - (a3 * b2)) * a1) + (((- (a1 * b3)) + (a3 * b1)) * a2)) + (((a1 * b2) - (a2 * b1)) * a3)) * p & 0. V = (((((a2 * b3) - (a3 * b2)) * b1) + (((- (a1 * b3)) + (a3 * b1)) * b2)) + (((a1 * b2) - (a2 * b1)) * b3)) * q ) by RLVECT_1:10;
then A18: 0. V = ((((((a2 * b3) - (a3 * b2)) * a1) + (((- (a1 * b3)) + (a3 * b1)) * a2)) + (((a1 * b2) - (a2 * b1)) * a3)) * p) + ((((((a2 * b3) - (a3 * b2)) * b1) + (((- (a1 * b3)) + (a3 * b1)) * b2)) + (((a1 * b2) - (a2 * b1)) * b3)) * q) ;
(((((a2 * b3) - (a3 * b2)) * a1) + (((- (a1 * b3)) + (a3 * b1)) * a2)) + (((a1 * b2) - (a2 * b1)) * a3)) * p = (((((a2 * b3) - (a3 * b2)) * a1) * p) + ((((- (a1 * b3)) + (a3 * b1)) * a2) * p)) + ((((a1 * b2) - (a2 * b1)) * a3) * p) by Lm3;
then 0. V = ((((((a2 * b3) - (a3 * b2)) * a1) * p) + ((((- (a1 * b3)) + (a3 * b1)) * a2) * p)) + ((((a1 * b2) - (a2 * b1)) * a3) * p)) + ((((((a2 * b3) - (a3 * b2)) * b1) * q) + ((((- (a1 * b3)) + (a3 * b1)) * b2) * q)) + ((((a1 * b2) - (a2 * b1)) * b3) * q)) by ;
then A19: 0. V = ((((((a2 * b3) - (a3 * b2)) * a1) * p) + ((((a2 * b3) - (a3 * b2)) * b1) * q)) + (((((- (a1 * b3)) + (a3 * b1)) * a2) * p) + ((((- (a1 * b3)) + (a3 * b1)) * b2) * q))) + (((((a1 * b2) - (a2 * b1)) * a3) * p) + ((((a1 * b2) - (a2 * b1)) * b3) * q)) by Lm4;
A20: ((((a1 * b2) - (a2 * b1)) * a3) * p) + ((((a1 * b2) - (a2 * b1)) * b3) * q) = ((a1 * b2) - (a2 * b1)) * ((a3 * p) + (b3 * q)) by Lm5;
( ((((a2 * b3) - (a3 * b2)) * a1) * p) + ((((a2 * b3) - (a3 * b2)) * b1) * q) = ((a2 * b3) - (a3 * b2)) * ((a1 * p) + (b1 * q)) & ((((- (a1 * b3)) + (a3 * b1)) * a2) * p) + ((((- (a1 * b3)) + (a3 * b1)) * b2) * q) = ((- (a1 * b3)) + (a3 * b1)) * ((a2 * p) + (b2 * q)) ) by Lm5;
hence u,v,w are_LinDep by A6, A8, A7, A19, A20, A9; :: thesis: verum