let V be RealLinearSpace; :: thesis: for o, u, v, w, u1, v1, w1, u2, v2, w2 being Element of V st not o is zero & u,v,w are_Prop_Vect & u2,v2,w2 are_Prop_Vect & u1,v1,w1 are_Prop_Vect & o,u,v,w,u2,v2,w2 lie_on_an_angle & o,u,v,w,u2,v2,w2 are_half_mutually_not_Prop & u,v2,w1 are_LinDep & u2,v,w1 are_LinDep & u,w2,v1 are_LinDep & w,u2,v1 are_LinDep & v,w2,u1 are_LinDep & w,v2,u1 are_LinDep holds

u1,v1,w1 are_LinDep

let o, u, v, w, u1, v1, w1, u2, v2, w2 be Element of V; :: thesis: ( not o is zero & u,v,w are_Prop_Vect & u2,v2,w2 are_Prop_Vect & u1,v1,w1 are_Prop_Vect & o,u,v,w,u2,v2,w2 lie_on_an_angle & o,u,v,w,u2,v2,w2 are_half_mutually_not_Prop & u,v2,w1 are_LinDep & u2,v,w1 are_LinDep & u,w2,v1 are_LinDep & w,u2,v1 are_LinDep & v,w2,u1 are_LinDep & w,v2,u1 are_LinDep implies u1,v1,w1 are_LinDep )

assume that

A1: not o is zero and

A2: u,v,w are_Prop_Vect and

A3: u2,v2,w2 are_Prop_Vect and

A4: u1,v1,w1 are_Prop_Vect and

A5: o,u,v,w,u2,v2,w2 lie_on_an_angle and

A6: o,u,v,w,u2,v2,w2 are_half_mutually_not_Prop and

A7: u,v2,w1 are_LinDep and

A8: u2,v,w1 are_LinDep and

A9: u,w2,v1 are_LinDep and

A10: w,u2,v1 are_LinDep and

A11: v,w2,u1 are_LinDep and

A12: w,v2,u1 are_LinDep ; :: thesis: u1,v1,w1 are_LinDep

A13: not u is zero by A2;

A14: not are_Prop u2,v2 by A6;

A15: not are_Prop o,v by A6;

A16: not are_Prop u,v by A6;

A17: o,u2,v2 are_LinDep by A5;

A18: ( not are_Prop o,w2 & not are_Prop u2,w2 ) by A6;

A19: not u2 is zero by A3;

A20: ( not are_Prop o,w & not are_Prop u,w ) by A6;

A21: o,u,w are_LinDep by A5;

A22: not are_Prop o,v2 by A6;

A23: o,u2,w2 are_LinDep by A5;

A24: not o,u,u2 are_LinDep by A5;

then A25: not are_Prop o,u by ANPROJ_1:12;

A26: not w is zero by A2;

then o,u,w are_Prop_Vect by A1, A13;

then consider a3, b3 being Real such that

A27: b3 * w = o + (a3 * u) and

a3 <> 0 and

A28: b3 <> 0 by A21, A20, A25, Th6;

A29: not are_Prop u2,o by A24, ANPROJ_1:12;

A30: not w2 is zero by A3;

then o,u2,w2 are_Prop_Vect by A1, A19;

then consider c3, d3 being Real such that

A31: d3 * w2 = o + (c3 * u2) and

c3 <> 0 and

A32: d3 <> 0 by A23, A18, A29, Th6;

A33: o,u,v are_LinDep by A5;

A34: not v2 is zero by A3;

then o,u2,v2 are_Prop_Vect by A1, A19;

then consider c2, d2 being Real such that

A35: d2 * v2 = o + (c2 * u2) and

A36: c2 <> 0 and

A37: d2 <> 0 by A17, A22, A14, A29, Th6;

A38: not v is zero by A2;

then o,u,v are_Prop_Vect by A1, A13;

then consider a2, b2 being Real such that

A39: b2 * v = o + (a2 * u) and

a2 <> 0 and

A40: b2 <> 0 by A33, A15, A16, A25, Th6;

set v9 = o + (a2 * u);

set w9 = o + (a3 * u);

set v29 = o + (c2 * u2);

set w29 = o + (c3 * u2);

A41: not o + (c2 * u2) is zero by A34, A35, A37, Lm20;

A42: not o + (a2 * u) is zero by A38, A39, A40, Lm20;

A43: not o + (a3 * u) is zero by A26, A27, A28, Lm20;

A44: not o + (c3 * u2) is zero by A30, A31, A32, Lm20;

A45: are_Prop w2,o + (c3 * u2) by A31, A32, Lm16;

then A46: u,o + (c3 * u2),v1 are_LinDep by A9, ANPROJ_1:4;

A47: are_Prop v,o + (a2 * u) by A39, A40, Lm16;

then A48: o + (a2 * u),o + (c3 * u2),u1 are_LinDep by A11, A45, ANPROJ_1:4;

A49: are_Prop v2,o + (c2 * u2) by A35, A37, Lm16;

then A50: u,o + (c2 * u2),w1 are_LinDep by A7, ANPROJ_1:4;

A51: are_Prop w,o + (a3 * u) by A27, A28, Lm16;

then A52: o + (a3 * u),o + (c2 * u2),u1 are_LinDep by A12, A49, ANPROJ_1:4;

not are_Prop u,v2

then consider A3, B3 being Real such that

A53: w1 = (A3 * u) + (B3 * (o + (c2 * u2))) by A13, A50, A41, ANPROJ_1:6;

not o,u2,v are_LinDep

then not are_Prop o + (a2 * u),o + (c3 * u2) by A39, A40, A31, A32, Lm21;

then consider A1, B1 being Real such that

A55: u1 = (A1 * (o + (a2 * u))) + (B1 * (o + (c3 * u2))) by A42, A44, A48, ANPROJ_1:6;

not o,u,v2 are_LinDep

then not are_Prop o + (a3 * u),o + (c2 * u2) by A27, A28, A35, A37, Lm21;

then consider A19, B19 being Real such that

A57: u1 = (A19 * (o + (a3 * u))) + (B19 * (o + (c2 * u2))) by A41, A43, A52, ANPROJ_1:6;

A58: u1 = (((A1 + B1) * o) + ((A1 * a2) * u)) + ((B1 * c3) * u2) by A55, Lm22;

A59: not are_Prop v2,w2 by A6;

A60: not are_Prop v,w by A6;

A61: ( not are_Prop o + (a2 * u),o + (a3 * u) & not are_Prop o + (c2 * u2),o + (c3 * u2) )

then consider A2, B2 being Real such that

A64: v1 = (A2 * u) + (B2 * (o + (c3 * u2))) by A13, A44, A46, ANPROJ_1:6;

u2,w,v1 are_LinDep by A10;

then A65: u2,o + (a3 * u),v1 are_LinDep by A51, ANPROJ_1:4;

not are_Prop u2,w by A24, A21, ANPROJ_1:4;

then not are_Prop u2,o + (a3 * u) by A27, A28, Lm17;

then consider A29, B29 being Real such that

A66: v1 = (A29 * u2) + (B29 * (o + (a3 * u))) by A19, A43, A65, ANPROJ_1:6;

A67: v1 = ((B2 * o) + (A2 * u)) + ((B2 * c3) * u2) by A64, Lm18;

A68: u2,o + (a2 * u),w1 are_LinDep by A8, A47, ANPROJ_1:4;

not are_Prop u2,v by A24, A33, ANPROJ_1:4;

then not are_Prop u2,o + (a2 * u) by A39, A40, Lm17;

then consider A39, B39 being Real such that

A69: w1 = (A39 * u2) + (B39 * (o + (a2 * u))) by A19, A68, A42, ANPROJ_1:6;

A70: w1 = ((B3 * o) + (A3 * u)) + ((B3 * c2) * u2) by A53, Lm18;

v1 = ((B29 * o) + ((B29 * a3) * u)) + (A29 * u2) by A66, Lm19;

then A71: ( B2 = B29 & A2 = B29 * a3 ) by A24, A67, ANPROJ_1:8;

w1 = ((B39 * o) + ((B39 * a2) * u)) + (A39 * u2) by A69, Lm19;

then A72: ( B3 = B39 & A3 = B39 * a2 ) by A24, A70, ANPROJ_1:8;

A73: u1 = (((A19 + B19) * o) + ((A19 * a3) * u)) + ((B19 * c2) * u2) by A57, Lm22;

then A74: B1 * c3 = B19 * c2 by A24, A58, ANPROJ_1:8;

( A1 + B1 = A19 + B19 & A1 * a2 = A19 * a3 ) by A24, A58, A73, ANPROJ_1:8;

then A75: A1 = (((a3 * c3) - (a3 * c2)) * (((a3 * c2) - (a2 * c2)) ")) * B1 by A36, A61, A74, Lm24;

set v19 = (o + (a3 * u)) + (c3 * u2);

set C2 = a2 * c2;

set C3 = - (a3 * c3);

set u19 = ((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u)) + (((c2 * c3) * (a3 - a2)) * u2);

set w19 = (o + (a2 * u)) + (c2 * u2);

A76: ((a2 * c2) * c3) + ((- (a3 * c3)) * c2) = (c2 * c3) * (a2 - a3) ;

( (a2 * c2) + (- (a3 * c3)) = (a2 * c2) - (a3 * c3) & ((a2 * c2) * a3) + ((- (a3 * c3)) * a2) = (a2 * a3) * (c2 - c3) ) ;

then ((1 * (((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u)) + (((c2 * c3) * (a3 - a2)) * u2))) + ((a2 * c2) * ((o + (a3 * u)) + (c3 * u2)))) + ((- (a3 * c3)) * ((o + (a2 * u)) + (c2 * u2))) = 0. V by A76, Lm28;

then A77: ((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u)) + (((c2 * c3) * (a3 - a2)) * u2),(o + (a3 * u)) + (c3 * u2),(o + (a2 * u)) + (c2 * u2) are_LinDep ;

A78: not v1 is zero by A4;

A79: B2 <> 0

then A80: are_Prop (o + (a3 * u)) + (c3 * u2),v1 by A79, Lm16;

A81: not w1 is zero by A4;

A82: B3 <> 0

then A83: are_Prop (o + (a2 * u)) + (c2 * u2),w1 by A82, Lm16;

A84: not u1 is zero by A4;

A85: B1 <> 0

then are_Prop ((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u)) + (((c2 * c3) * (a3 - a2)) * u2),u1 by A36, A61, A85, Lm16, Lm25;

hence u1,v1,w1 are_LinDep by A83, A80, A77, ANPROJ_1:4; :: thesis: verum

u1,v1,w1 are_LinDep

let o, u, v, w, u1, v1, w1, u2, v2, w2 be Element of V; :: thesis: ( not o is zero & u,v,w are_Prop_Vect & u2,v2,w2 are_Prop_Vect & u1,v1,w1 are_Prop_Vect & o,u,v,w,u2,v2,w2 lie_on_an_angle & o,u,v,w,u2,v2,w2 are_half_mutually_not_Prop & u,v2,w1 are_LinDep & u2,v,w1 are_LinDep & u,w2,v1 are_LinDep & w,u2,v1 are_LinDep & v,w2,u1 are_LinDep & w,v2,u1 are_LinDep implies u1,v1,w1 are_LinDep )

assume that

A1: not o is zero and

A2: u,v,w are_Prop_Vect and

A3: u2,v2,w2 are_Prop_Vect and

A4: u1,v1,w1 are_Prop_Vect and

A5: o,u,v,w,u2,v2,w2 lie_on_an_angle and

A6: o,u,v,w,u2,v2,w2 are_half_mutually_not_Prop and

A7: u,v2,w1 are_LinDep and

A8: u2,v,w1 are_LinDep and

A9: u,w2,v1 are_LinDep and

A10: w,u2,v1 are_LinDep and

A11: v,w2,u1 are_LinDep and

A12: w,v2,u1 are_LinDep ; :: thesis: u1,v1,w1 are_LinDep

A13: not u is zero by A2;

A14: not are_Prop u2,v2 by A6;

A15: not are_Prop o,v by A6;

A16: not are_Prop u,v by A6;

A17: o,u2,v2 are_LinDep by A5;

A18: ( not are_Prop o,w2 & not are_Prop u2,w2 ) by A6;

A19: not u2 is zero by A3;

A20: ( not are_Prop o,w & not are_Prop u,w ) by A6;

A21: o,u,w are_LinDep by A5;

A22: not are_Prop o,v2 by A6;

A23: o,u2,w2 are_LinDep by A5;

A24: not o,u,u2 are_LinDep by A5;

then A25: not are_Prop o,u by ANPROJ_1:12;

A26: not w is zero by A2;

then o,u,w are_Prop_Vect by A1, A13;

then consider a3, b3 being Real such that

A27: b3 * w = o + (a3 * u) and

a3 <> 0 and

A28: b3 <> 0 by A21, A20, A25, Th6;

A29: not are_Prop u2,o by A24, ANPROJ_1:12;

A30: not w2 is zero by A3;

then o,u2,w2 are_Prop_Vect by A1, A19;

then consider c3, d3 being Real such that

A31: d3 * w2 = o + (c3 * u2) and

c3 <> 0 and

A32: d3 <> 0 by A23, A18, A29, Th6;

A33: o,u,v are_LinDep by A5;

A34: not v2 is zero by A3;

then o,u2,v2 are_Prop_Vect by A1, A19;

then consider c2, d2 being Real such that

A35: d2 * v2 = o + (c2 * u2) and

A36: c2 <> 0 and

A37: d2 <> 0 by A17, A22, A14, A29, Th6;

A38: not v is zero by A2;

then o,u,v are_Prop_Vect by A1, A13;

then consider a2, b2 being Real such that

A39: b2 * v = o + (a2 * u) and

a2 <> 0 and

A40: b2 <> 0 by A33, A15, A16, A25, Th6;

set v9 = o + (a2 * u);

set w9 = o + (a3 * u);

set v29 = o + (c2 * u2);

set w29 = o + (c3 * u2);

A41: not o + (c2 * u2) is zero by A34, A35, A37, Lm20;

A42: not o + (a2 * u) is zero by A38, A39, A40, Lm20;

A43: not o + (a3 * u) is zero by A26, A27, A28, Lm20;

A44: not o + (c3 * u2) is zero by A30, A31, A32, Lm20;

A45: are_Prop w2,o + (c3 * u2) by A31, A32, Lm16;

then A46: u,o + (c3 * u2),v1 are_LinDep by A9, ANPROJ_1:4;

A47: are_Prop v,o + (a2 * u) by A39, A40, Lm16;

then A48: o + (a2 * u),o + (c3 * u2),u1 are_LinDep by A11, A45, ANPROJ_1:4;

A49: are_Prop v2,o + (c2 * u2) by A35, A37, Lm16;

then A50: u,o + (c2 * u2),w1 are_LinDep by A7, ANPROJ_1:4;

A51: are_Prop w,o + (a3 * u) by A27, A28, Lm16;

then A52: o + (a3 * u),o + (c2 * u2),u1 are_LinDep by A12, A49, ANPROJ_1:4;

not are_Prop u,v2

proof

then
not are_Prop u,o + (c2 * u2)
by A35, A37, Lm17;
assume
are_Prop u,v2
; :: thesis: contradiction

then o,u2,u are_LinDep by A17, ANPROJ_1:4;

hence contradiction by A24, ANPROJ_1:5; :: thesis: verum

end;then o,u2,u are_LinDep by A17, ANPROJ_1:4;

hence contradiction by A24, ANPROJ_1:5; :: thesis: verum

then consider A3, B3 being Real such that

A53: w1 = (A3 * u) + (B3 * (o + (c2 * u2))) by A13, A50, A41, ANPROJ_1:6;

not o,u2,v are_LinDep

proof

then
not are_Prop v,w2
by A23, ANPROJ_1:4;
assume
o,u2,v are_LinDep
; :: thesis: contradiction

then A54: o,v,u2 are_LinDep by ANPROJ_1:5;

( o,v,u are_LinDep & o,v,o are_LinDep ) by A33, ANPROJ_1:5, ANPROJ_1:11;

hence contradiction by A1, A38, A24, A15, A54, ANPROJ_1:14; :: thesis: verum

end;then A54: o,v,u2 are_LinDep by ANPROJ_1:5;

( o,v,u are_LinDep & o,v,o are_LinDep ) by A33, ANPROJ_1:5, ANPROJ_1:11;

hence contradiction by A1, A38, A24, A15, A54, ANPROJ_1:14; :: thesis: verum

then not are_Prop o + (a2 * u),o + (c3 * u2) by A39, A40, A31, A32, Lm21;

then consider A1, B1 being Real such that

A55: u1 = (A1 * (o + (a2 * u))) + (B1 * (o + (c3 * u2))) by A42, A44, A48, ANPROJ_1:6;

not o,u,v2 are_LinDep

proof

then
not are_Prop v2,w
by A21, ANPROJ_1:4;
assume
o,u,v2 are_LinDep
; :: thesis: contradiction

then A56: o,v2,u are_LinDep by ANPROJ_1:5;

( o,v2,u2 are_LinDep & o,v2,o are_LinDep ) by A17, ANPROJ_1:5, ANPROJ_1:11;

hence contradiction by A1, A34, A24, A22, A56, ANPROJ_1:14; :: thesis: verum

end;then A56: o,v2,u are_LinDep by ANPROJ_1:5;

( o,v2,u2 are_LinDep & o,v2,o are_LinDep ) by A17, ANPROJ_1:5, ANPROJ_1:11;

hence contradiction by A1, A34, A24, A22, A56, ANPROJ_1:14; :: thesis: verum

then not are_Prop o + (a3 * u),o + (c2 * u2) by A27, A28, A35, A37, Lm21;

then consider A19, B19 being Real such that

A57: u1 = (A19 * (o + (a3 * u))) + (B19 * (o + (c2 * u2))) by A41, A43, A52, ANPROJ_1:6;

A58: u1 = (((A1 + B1) * o) + ((A1 * a2) * u)) + ((B1 * c3) * u2) by A55, Lm22;

A59: not are_Prop v2,w2 by A6;

A60: not are_Prop v,w by A6;

A61: ( not are_Prop o + (a2 * u),o + (a3 * u) & not are_Prop o + (c2 * u2),o + (c3 * u2) )

proof

hence contradiction by A63, A62; :: thesis: verum

end;

not are_Prop u,w2
A62: now :: thesis: not are_Prop o + (c2 * u2),o + (c3 * u2)

assume
are_Prop o + (c2 * u2),o + (c3 * u2)
; :: thesis: contradiction

then are_Prop v2,o + (c3 * u2) by A49, ANPROJ_1:2;

hence contradiction by A59, A45, ANPROJ_1:2; :: thesis: verum

end;then are_Prop v2,o + (c3 * u2) by A49, ANPROJ_1:2;

hence contradiction by A59, A45, ANPROJ_1:2; :: thesis: verum

A63: now :: thesis: not are_Prop o + (a2 * u),o + (a3 * u)

assume
( are_Prop o + (a2 * u),o + (a3 * u) or are_Prop o + (c2 * u2),o + (c3 * u2) )
; :: thesis: contradictionassume
are_Prop o + (a2 * u),o + (a3 * u)
; :: thesis: contradiction

then are_Prop v,o + (a3 * u) by A47, ANPROJ_1:2;

hence contradiction by A60, A51, ANPROJ_1:2; :: thesis: verum

end;then are_Prop v,o + (a3 * u) by A47, ANPROJ_1:2;

hence contradiction by A60, A51, ANPROJ_1:2; :: thesis: verum

hence contradiction by A63, A62; :: thesis: verum

proof

then
not are_Prop u,o + (c3 * u2)
by A31, A32, Lm17;
assume
are_Prop u,w2
; :: thesis: contradiction

then o,u2,u are_LinDep by A23, ANPROJ_1:4;

hence contradiction by A24, ANPROJ_1:5; :: thesis: verum

end;then o,u2,u are_LinDep by A23, ANPROJ_1:4;

hence contradiction by A24, ANPROJ_1:5; :: thesis: verum

then consider A2, B2 being Real such that

A64: v1 = (A2 * u) + (B2 * (o + (c3 * u2))) by A13, A44, A46, ANPROJ_1:6;

u2,w,v1 are_LinDep by A10;

then A65: u2,o + (a3 * u),v1 are_LinDep by A51, ANPROJ_1:4;

not are_Prop u2,w by A24, A21, ANPROJ_1:4;

then not are_Prop u2,o + (a3 * u) by A27, A28, Lm17;

then consider A29, B29 being Real such that

A66: v1 = (A29 * u2) + (B29 * (o + (a3 * u))) by A19, A43, A65, ANPROJ_1:6;

A67: v1 = ((B2 * o) + (A2 * u)) + ((B2 * c3) * u2) by A64, Lm18;

A68: u2,o + (a2 * u),w1 are_LinDep by A8, A47, ANPROJ_1:4;

not are_Prop u2,v by A24, A33, ANPROJ_1:4;

then not are_Prop u2,o + (a2 * u) by A39, A40, Lm17;

then consider A39, B39 being Real such that

A69: w1 = (A39 * u2) + (B39 * (o + (a2 * u))) by A19, A68, A42, ANPROJ_1:6;

A70: w1 = ((B3 * o) + (A3 * u)) + ((B3 * c2) * u2) by A53, Lm18;

v1 = ((B29 * o) + ((B29 * a3) * u)) + (A29 * u2) by A66, Lm19;

then A71: ( B2 = B29 & A2 = B29 * a3 ) by A24, A67, ANPROJ_1:8;

w1 = ((B39 * o) + ((B39 * a2) * u)) + (A39 * u2) by A69, Lm19;

then A72: ( B3 = B39 & A3 = B39 * a2 ) by A24, A70, ANPROJ_1:8;

A73: u1 = (((A19 + B19) * o) + ((A19 * a3) * u)) + ((B19 * c2) * u2) by A57, Lm22;

then A74: B1 * c3 = B19 * c2 by A24, A58, ANPROJ_1:8;

( A1 + B1 = A19 + B19 & A1 * a2 = A19 * a3 ) by A24, A58, A73, ANPROJ_1:8;

then A75: A1 = (((a3 * c3) - (a3 * c2)) * (((a3 * c2) - (a2 * c2)) ")) * B1 by A36, A61, A74, Lm24;

set v19 = (o + (a3 * u)) + (c3 * u2);

set C2 = a2 * c2;

set C3 = - (a3 * c3);

set u19 = ((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u)) + (((c2 * c3) * (a3 - a2)) * u2);

set w19 = (o + (a2 * u)) + (c2 * u2);

A76: ((a2 * c2) * c3) + ((- (a3 * c3)) * c2) = (c2 * c3) * (a2 - a3) ;

( (a2 * c2) + (- (a3 * c3)) = (a2 * c2) - (a3 * c3) & ((a2 * c2) * a3) + ((- (a3 * c3)) * a2) = (a2 * a3) * (c2 - c3) ) ;

then ((1 * (((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u)) + (((c2 * c3) * (a3 - a2)) * u2))) + ((a2 * c2) * ((o + (a3 * u)) + (c3 * u2)))) + ((- (a3 * c3)) * ((o + (a2 * u)) + (c2 * u2))) = 0. V by A76, Lm28;

then A77: ((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u)) + (((c2 * c3) * (a3 - a2)) * u2),(o + (a3 * u)) + (c3 * u2),(o + (a2 * u)) + (c2 * u2) are_LinDep ;

A78: not v1 is zero by A4;

A79: B2 <> 0

proof

v1 = B2 * ((o + (a3 * u)) + (c3 * u2))
by A67, A71, Lm29;
assume
not B2 <> 0
; :: thesis: contradiction

then v1 = (0. V) + (0 * (o + (c3 * u2))) by A64, A71, RLVECT_1:10

.= (0. V) + (0. V) by RLVECT_1:10

.= 0. V by RLVECT_1:4 ;

hence contradiction by A78; :: thesis: verum

end;then v1 = (0. V) + (0 * (o + (c3 * u2))) by A64, A71, RLVECT_1:10

.= (0. V) + (0. V) by RLVECT_1:10

.= 0. V by RLVECT_1:4 ;

hence contradiction by A78; :: thesis: verum

then A80: are_Prop (o + (a3 * u)) + (c3 * u2),v1 by A79, Lm16;

A81: not w1 is zero by A4;

A82: B3 <> 0

proof

w1 = B3 * ((o + (a2 * u)) + (c2 * u2))
by A70, A72, Lm29;
assume
not B3 <> 0
; :: thesis: contradiction

then w1 = (0. V) + (0 * (o + (c2 * u2))) by A53, A72, RLVECT_1:10

.= (0. V) + (0. V) by RLVECT_1:10

.= 0. V by RLVECT_1:4 ;

hence contradiction by A81; :: thesis: verum

end;then w1 = (0. V) + (0 * (o + (c2 * u2))) by A53, A72, RLVECT_1:10

.= (0. V) + (0. V) by RLVECT_1:10

.= 0. V by RLVECT_1:4 ;

hence contradiction by A81; :: thesis: verum

then A83: are_Prop (o + (a2 * u)) + (c2 * u2),w1 by A82, Lm16;

A84: not u1 is zero by A4;

A85: B1 <> 0

proof

u1 = (B1 * (((a3 * c2) - (a2 * c2)) ")) * (((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u)) + (((c2 * c3) * (a3 - a2)) * u2))
by A36, A61, A58, A75, Lm26;
assume
not B1 <> 0
; :: thesis: contradiction

then u1 = (0. V) + (0 * (o + (c3 * u2))) by A55, A75, RLVECT_1:10

.= (0. V) + (0. V) by RLVECT_1:10

.= 0. V by RLVECT_1:4 ;

hence contradiction by A84; :: thesis: verum

end;then u1 = (0. V) + (0 * (o + (c3 * u2))) by A55, A75, RLVECT_1:10

.= (0. V) + (0. V) by RLVECT_1:10

.= 0. V by RLVECT_1:4 ;

hence contradiction by A84; :: thesis: verum

then are_Prop ((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u)) + (((c2 * c3) * (a3 - a2)) * u2),u1 by A36, A61, A85, Lm16, Lm25;

hence u1,v1,w1 are_LinDep by A83, A80, A77, ANPROJ_1:4; :: thesis: verum