let V be RealLinearSpace; :: thesis:
let o, u, v, w, u2, v2, w2, u1, v1, w1 be Element of V; :: thesis:
assume that
A1: ( not o is zero & u,v,w are_Prop_Vect & u2,v2,w2 are_Prop_Vect & u1,v1,w1 are_Prop_Vect ) and
A2: o,u,v,w,u2,v2,w2 are_perspective and
A3: ( not are_Prop o,u2 & not are_Prop o,v2 & not are_Prop o,w2 & not are_Prop u,u2 & not are_Prop v,v2 & not are_Prop w,w2 ) and
A4: ( not o,u,v are_LinDep & not o,u,w are_LinDep & not o,v,w are_LinDep ) and
A5: ( u,v,w,u1,v1,w1 lie_on_a_triangle & u2,v2,w2,u1,v1,w1 lie_on_a_triangle ) ; :: thesis:
A6: ( not o is zero & not u is zero & not v is zero & not w is zero & not u2 is zero & not v2 is zero & not w2 is zero & not u1 is zero & not v1 is zero & not w1 is zero ) by A1, Def1;
A7: ( o,u,u2 are_LinDep & o,v,v2 are_LinDep & o,w,w2 are_LinDep ) by A2, Def3;
A8: ( u,v,w1 are_LinDep & u,w,v1 are_LinDep & v,w,u1 are_LinDep & u2,v2,w1 are_LinDep & u2,w2,v1 are_LinDep & v2,w2,u1 are_LinDep ) by A5, Def2;
A9: ( not are_Prop o,u & not are_Prop o,v & not are_Prop w,o ) by A4, ANPROJ_1:16;
A10: ( o,u,u2 are_Prop_Vect & o,v,v2 are_Prop_Vect & o,w,w2 are_Prop_Vect ) by A6, Def1;
then consider a1, b1 being Real such that
A11: ( b1 * u2 = o + (a1 * u) & a1 <> 0 & b1 <> 0 ) by A3, A7, A9, Th6;
consider a2, b2 being Real such that
A12: ( b2 * v2 = o + (a2 * v) & a2 <> 0 & b2 <> 0 ) by A3, A7, A9, A10, Th6;
consider a3, b3 being Real such that
A13: ( b3 * w2 = o + (a3 * w) & a3 <> 0 & b3 <> 0 ) by A3, A7, A9, A10, Th6;
set u2' = o + (a1 * u);
set v2' = o + (a2 * v);
set w2' = o + (a3 * w);
A14: ( u,v,w1 are_Prop_Vect & u,w,v1 are_Prop_Vect & v,w,u1 are_Prop_Vect & u2,v2,w1 are_Prop_Vect & u2,w2,v1 are_Prop_Vect & v2,w2,u1 are_Prop_Vect ) by A6, Def1;
A15: ( not are_Prop u,v & not are_Prop u,w & not are_Prop v,w ) by A4, ANPROJ_1:17;
then consider c3, d3 being Real such that
A16: w1 = (c3 * u) + (d3 * v) by A8, A14, Th7;
consider c2, d2 being Real such that
A17: v1 = (c2 * u) + (d2 * w) by A8, A14, A15, Th7;
consider c1, d1 being Real such that
A18: u1 = (c1 * v) + (d1 * w) by A8, A14, A15, Th7;
A19: ( o + (a1 * u),o + (a2 * v),w1 are_LinDep & o + (a1 * u),o + (a3 * w),v1 are_LinDep & o + (a2 * v),o + (a3 * w),u1 are_LinDep )

proof

( are_Prop u2,o + (a1 * u) & are_Prop v2,o + (a2 * v) & are_Prop w2,o + (a3 * w) ) by A11, A12, A13, Lm9;
hence ( o + (a1 * u),o + (a2 * v),w1 are_LinDep & o + (a1 * u),o + (a3 * w),v1 are_LinDep & o + (a2 * v),o + (a3 * w),u1 are_LinDep ) by A8, ANPROJ_1:9; :: thesis:

end;

A20: ( not are_Prop o + (a1 * u),o + (a2 * v) & not are_Prop o + (a1 * u),o + (a3 * w) & not are_Prop o + (a2 * v),o + (a3 * w) ) by A4, A11, A12, Lm10;
( not o + (a1 * u) is zero & not o + (a2 * v) is zero & not o + (a3 * w) is zero ) by A6, A11, A12, A13, Lm11;
then A21: ( o + (a1 * u),o + (a2 * v),w1 are_Prop_Vect & o + (a1 * u),o + (a3 * w),v1 are_Prop_Vect & o + (a2 * v),o + (a3 * w),u1 are_Prop_Vect ) by A6, Def1;
then consider A3, B3 being Real such that
A22: w1 = (A3 * (o + (a1 * u))) + (B3 * (o + (a2 * v))) by A19, A20, Th7;
consider A2, B2 being Real such that
A23: v1 = (A2 * (o + (a1 * u))) + (B2 * (o + (a3 * w))) by A19, A20, A21, Th7;
consider A1, B1 being Real such that
A24: u1 = (A1 * (o + (a2 * v))) + (B1 * (o + (a3 * w))) by A19, A20, A21, Th7;
A25: ( w1 = (((A3 + B3) * o) + ((A3 * a1) * u)) + ((B3 * a2) * v) & v1 = (((A2 + B2) * o) + ((A2 * a1) * u)) + ((B2 * a3) * w) & u1 = (((A1 + B1) * o) + ((A1 * a2) * v)) + ((B1 * a3) * w) ) by A22, A23, A24, Lm12;
( u1 = ((0 * o) + (c1 * v)) + (d1 * w) & v1 = ((0 * o) + (c2 * u)) + (d2 * w) & w1 = ((0 * o) + (c3 * u)) + (d3 * v) ) by A16, A17, A18, Lm13;
then A26: ( A1 + B1 = 0 & A2 + B2 = 0 & A3 + B3 = 0 ) by A4, A25, ANPROJ_1:13;
then A27: ( B1 = - A1 & B2 = - A2 & B3 = - A3 ) ;
A28: ( A1 <> 0 & A2 <> 0 & A3 <> 0 )

proof

assume A29: ( not A1 <> 0 or not A2 <> 0 or not A3 <> 0 ) ; :: thesis:

A30: now

assume A1 = 0 ; :: thesis:
then u1 = 0. V by A24, A26, Lm14;
hence contradiction by A6, STRUCT_0:def 15; :: thesis:

end;

A31: now

assume A2 = 0 ; :: thesis:
then v1 = 0. V by A23, A26, Lm14;
hence contradiction by A6, STRUCT_0:def 15; :: thesis:

end;

now

assume A3 = 0 ; :: thesis:
then w1 = 0. V by A22, A26, Lm14;
hence contradiction by A6, STRUCT_0:def 15; :: thesis:

end;

hence contradiction by A29, A30, A31; :: thesis:

end;

set u1' = (a2 * v) - (a3 * w);
set v1' = (a1 * u) - (a3 * w);
set w1' = (a1 * u) - (a2 * v);
( u1 = A1 * ((a2 * v) - (a3 * w)) & v1 = A2 * ((a1 * u) - (a3 * w)) & w1 = A3 * ((a1 * u) - (a2 * v)) ) by A25, A27, Lm15;
then A32: ( are_Prop (a2 * v) - (a3 * w),u1 & are_Prop (a1 * u) - (a3 * w),v1 & are_Prop (a1 * u) - (a2 * v),w1 ) by A28, Lm9;
((1 * ((a2 * v) - (a3 * w))) + ((- 1) * ((a1 * u) - (a3 * w)))) + (1 * ((a1 * u) - (a2 * v))) = (((a2 * v) - (a3 * w)) + ((- 1) * ((a1 * u) - (a3 * w)))) + (1 * ((a1 * u) - (a2 * v))) by RLVECT_1:def 9
.= (((a2 * v) - (a3 * w)) + ((- 1) * ((a1 * u) - (a3 * w)))) + ((a1 * u) - (a2 * v)) by RLVECT_1:def 9
.= (((a2 * v) - (a3 * w)) + (- ((a1 * u) - (a3 * w)))) + ((a1 * u) - (a2 * v)) by RLVECT_1:29
.= (((a2 * v) + (- (a3 * w))) + ((a3 * w) + (- (a1 * u)))) + ((a1 * u) - (a2 * v)) by RLVECT_1:47
.= ((((a2 * v) + (- (a3 * w))) + (a3 * w)) + (- (a1 * u))) + ((a1 * u) + (- (a2 * v))) by RLVECT_1:def 6
.= (((a2 * v) + ((- (a3 * w)) + (a3 * w))) + (- (a1 * u))) + ((a1 * u) + (- (a2 * v))) by RLVECT_1:def 6
.= (((a2 * v) + (0. V)) + (- (a1 * u))) + ((a1 * u) + (- (a2 * v))) by RLVECT_1:16
.= ((a2 * v) + (- (a1 * u))) + ((a1 * u) + (- (a2 * v))) by RLVECT_1:10
.= (a2 * v) + ((- (a1 * u)) + ((a1 * u) + (- (a2 * v)))) by RLVECT_1:def 6
.= (a2 * v) + (((- (a1 * u)) + (a1 * u)) + (- (a2 * v))) by RLVECT_1:def 6
.= (a2 * v) + ((0. V) + (- (a2 * v))) by RLVECT_1:16
.= (a2 * v) + (- (a2 * v)) by RLVECT_1:10
.= 0. V by RLVECT_1:16 ;
then (a2 * v) - (a3 * w),(a1 * u) - (a3 * w),(a1 * u) - (a2 * v) are_LinDep by ANPROJ_1:def 3;
hence u1,v1,w1 are_LinDep by A32, ANPROJ_1:9; :: thesis: