let V be RealLinearSpace; :: thesis: for x, y being VECTOR of V st Gen x,y holds
ex u, v, w being VECTOR of V st
( u,v,u,w are_COrte_wrt x,y & ( for v1, w1 being VECTOR of V holds
( not v1,w1,u,v are_COrte_wrt x,y or ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 ) ) )
let x, y be VECTOR of V; :: thesis: ( Gen x,y implies ex u, v, w being VECTOR of V st
( u,v,u,w are_COrte_wrt x,y & ( for v1, w1 being VECTOR of V holds
( not v1,w1,u,v are_COrte_wrt x,y or ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 ) ) ) )
assume A1: Gen x,y ; :: thesis: ex u, v, w being VECTOR of V st
( u,v,u,w are_COrte_wrt x,y & ( for v1, w1 being VECTOR of V holds
( not v1,w1,u,v are_COrte_wrt x,y or ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 ) ) )
( Gen x,y implies ex u, v being VECTOR of V st u <> v )

proof

assume A2: Gen x,y ; :: thesis: ex u, v being VECTOR of V st u <> v
take x ; :: thesis: ex v being VECTOR of V st x <> v
take 0. V ; :: thesis: x <> 0. V
thus x <> 0. V by A2, Lm4; :: thesis: verum

end;

then consider u, v being VECTOR of V such that
A3: u <> v by A1;
take u ; :: thesis: ex v, w being VECTOR of V st
( u,v,u,w are_COrte_wrt x,y & ( for v1, w1 being VECTOR of V holds
( not v1,w1,u,v are_COrte_wrt x,y or ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 ) ) )
take v ; :: thesis: ex w being VECTOR of V st
( u,v,u,w are_COrte_wrt x,y & ( for v1, w1 being VECTOR of V holds
( not v1,w1,u,v are_COrte_wrt x,y or ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 ) ) )
consider w being VECTOR of V such that
A4: w <> u and
A5: u,v,u,w are_COrte_wrt x,y by A1, Th40;
take w ; :: thesis: ( u,v,u,w are_COrte_wrt x,y & ( for v1, w1 being VECTOR of V holds
( not v1,w1,u,v are_COrte_wrt x,y or ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 ) ) )
thus u,v,u,w are_COrte_wrt x,y by A5; :: thesis: for v1, w1 being VECTOR of V holds
( not v1,w1,u,v are_COrte_wrt x,y or ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 )
A6: Orte x,y,u, Orte x,y,v // u,w by A5, Def3;
let v1, w1 be VECTOR of V; :: thesis: ( not v1,w1,u,v are_COrte_wrt x,y or ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 )
assume v1,w1,u,v are_COrte_wrt x,y ; :: thesis: ( ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 )
then A7: Orte x,y,v1, Orte x,y,w1 // u,v by Def3;

now

assume A8: v1 <> w1 ; :: thesis: ( ( v1,w1,u,w are_COrte_wrt x,y or v1,w1,w,u are_COrte_wrt x,y ) implies ex a, b being Real st
( ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 ) )
assume ( v1,w1,u,w are_COrte_wrt x,y or v1,w1,w,u are_COrte_wrt x,y ) ; :: thesis: ex a, b being Real st
( ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 )
then ( Orte x,y,v1, Orte x,y,w1 // u,w or Orte x,y,v1, Orte x,y,w1 // w,u ) by Def3;
then ( u,v // u,w or u,v // w,u ) by A1, A7, A8, Th13, ANALOAF:20;
then ( Orte x,y,u, Orte x,y,v // Orte x,y,u, Orte x,y,w or Orte x,y,u, Orte x,y,v // Orte x,y,w, Orte x,y,u ) by A1, Th16;
then ( u,w // Orte x,y,u, Orte x,y,w or u,w // Orte x,y,w, Orte x,y,u ) by A1, A3, A6, Th13, ANALOAF:20;
then consider a, b being Real such that
A9: a * (w - u) = b * ((Orte x,y,w) - (Orte x,y,u)) and
A10: ( a <> 0 or b <> 0 ) by ANALMETR:18;
take a = a; :: thesis: ex b being Real st
( ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 )
take b = b; :: thesis: ( ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 )
a * (w - u) = b * (Orte x,y,(w - u)) by A1, A9, Th11;
then A11: a * (((pr1 x,y,(w - u)) * x) + ((pr2 x,y,(w - u)) * y)) = b * (Orte x,y,(w - u)) by A1, Lm5;

A12: now

assume A13: a <> 0 ; :: thesis: ( ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 )
A14: pr2 x,y,(w - u) <> 0

proof

assume A15: not pr2 x,y,(w - u) <> 0 ; :: thesis: contradiction
then a * (((pr1 x,y,(w - u)) * x) + ((pr2 x,y,(w - u)) * y)) = ((b * 0 ) * x) + ((b * (- (pr1 x,y,(w - u)))) * y) by A11, Lm2;
then ((a * (pr1 x,y,(w - u))) * x) + ((a * (pr2 x,y,(w - u))) * y) = ((b * 0 ) * x) + ((b * (- (pr1 x,y,(w - u)))) * y) by Lm2;
then a * (pr1 x,y,(w - u)) = 0 by A1, Lm3;
then pr1 x,y,(w - u) = 0 by A13, XCMPLX_1:6;
then w - u = (0 * x) + (0 * y) by A1, A15, Lm5
.= (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 A4, RLVECT_1:35; :: thesis: verum

end;

((a " ) * a) * (((pr1 x,y,(w - u)) * x) + ((pr2 x,y,(w - u)) * y)) = (a " ) * (b * (((pr2 x,y,(w - u)) * x) + ((- (pr1 x,y,(w - u))) * y))) by A11, RLVECT_1:def 9;
then ((a " ) * a) * (((pr1 x,y,(w - u)) * x) + ((pr2 x,y,(w - u)) * y)) = ((a " ) * b) * (((pr2 x,y,(w - u)) * x) + ((- (pr1 x,y,(w - u))) * y)) by RLVECT_1:def 9;
then 1 * (((pr1 x,y,(w - u)) * x) + ((pr2 x,y,(w - u)) * y)) = ((a " ) * b) * (((pr2 x,y,(w - u)) * x) + ((- (pr1 x,y,(w - u))) * y)) by A13, XCMPLX_0:def 7;
then ((pr1 x,y,(w - u)) * x) + ((pr2 x,y,(w - u)) * y) = ((a " ) * b) * (((pr2 x,y,(w - u)) * x) + ((- (pr1 x,y,(w - u))) * y)) by RLVECT_1:def 9;
then A16: ((pr1 x,y,(w - u)) * x) + ((pr2 x,y,(w - u)) * y) = ((((a " ) * b) * (pr2 x,y,(w - u))) * x) + ((((a " ) * b) * (- (pr1 x,y,(w - u)))) * y) by Lm2;
then pr1 x,y,(w - u) = ((a " ) * b) * (pr2 x,y,(w - u)) by A1, Lm3;
then A17: pr2 x,y,(w - u) = - (((a " ) * b) * (((a " ) * b) * (pr2 x,y,(w - u)))) by A1, A16, Lm3;
- (((pr2 x,y,(w - u)) " ) * (pr2 x,y,(w - u))) = ((pr2 x,y,(w - u)) " ) * (- (pr2 x,y,(w - u)))
.= ((pr2 x,y,(w - u)) " ) * (((a " ) * b) * (((a " ) * b) * (pr2 x,y,(w - u)))) by A17 ;
then - 1 = (((pr2 x,y,(w - u)) " ) * (pr2 x,y,(w - u))) * (((a " ) * b) * ((a " ) * b)) by A14, XCMPLX_0:def 7;
then - 1 = 1 * (((a " ) * b) * ((a " ) * b)) by A14, XCMPLX_0:def 7;
hence ( ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 ) by XREAL_1:65; :: thesis: verum

end;

now

assume A18: b <> 0 ; :: thesis: ( ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 )
A19: pr2 x,y,(w - u) <> 0

proof

assume A20: not pr2 x,y,(w - u) <> 0 ; :: thesis: contradiction
then a * (((pr1 x,y,(w - u)) * x) + (0 * y)) = ((b * 0 ) * x) + ((b * (- (pr1 x,y,(w - u)))) * y) by A11, Lm2;
then ((a * (pr1 x,y,(w - u))) * x) + ((a * 0 ) * y) = ((b * 0 ) * x) + ((b * (- (pr1 x,y,(w - u)))) * y) by Lm2;
then b * (- (pr1 x,y,(w - u))) = 0 by A1, Lm3;
then - (pr1 x,y,(w - u)) = 0 by A18, XCMPLX_1:6;
then w - u = (0 * x) + ((- 0 ) * y) by A1, A20, Lm5
.= (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 A4, RLVECT_1:35; :: thesis: verum

end;

(b " ) * (a * (((pr1 x,y,(w - u)) * x) + ((pr2 x,y,(w - u)) * y))) = ((b " ) * b) * (((pr2 x,y,(w - u)) * x) + ((- (pr1 x,y,(w - u))) * y)) by A11, RLVECT_1:def 9;
then ((b " ) * a) * (((pr1 x,y,(w - u)) * x) + ((pr2 x,y,(w - u)) * y)) = ((b " ) * b) * (((pr2 x,y,(w - u)) * x) + ((- (pr1 x,y,(w - u))) * y)) by RLVECT_1:def 9;
then ((b " ) * a) * (((pr1 x,y,(w - u)) * x) + ((pr2 x,y,(w - u)) * y)) = 1 * (((pr2 x,y,(w - u)) * x) + ((- (pr1 x,y,(w - u))) * y)) by A18, XCMPLX_0:def 7;
then ((b " ) * a) * (((pr1 x,y,(w - u)) * x) + ((pr2 x,y,(w - u)) * y)) = ((pr2 x,y,(w - u)) * x) + ((- (pr1 x,y,(w - u))) * y) by RLVECT_1:def 9;
then A21: ((((b " ) * a) * (pr1 x,y,(w - u))) * x) + ((((b " ) * a) * (pr2 x,y,(w - u))) * y) = ((pr2 x,y,(w - u)) * x) + ((- (pr1 x,y,(w - u))) * y) by Lm2;
then ((b " ) * a) * (pr2 x,y,(w - u)) = - (pr1 x,y,(w - u)) by A1, Lm3;
then A22: pr2 x,y,(w - u) = ((b " ) * a) * (- (((b " ) * a) * (pr2 x,y,(w - u)))) by A1, A21, Lm3;
- (((pr2 x,y,(w - u)) " ) * (pr2 x,y,(w - u))) = ((pr2 x,y,(w - u)) " ) * (- (pr2 x,y,(w - u)))
.= ((pr2 x,y,(w - u)) " ) * (((b " ) * a) * (((b " ) * a) * (pr2 x,y,(w - u)))) by A22 ;
then - 1 = (((pr2 x,y,(w - u)) " ) * (pr2 x,y,(w - u))) * (((b " ) * a) * ((b " ) * a)) by A19, XCMPLX_0:def 7;
then - 1 = 1 * (((b " ) * a) * ((b " ) * a)) by A19, XCMPLX_0:def 7;
hence ( ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 ) by XREAL_1:65; :: thesis: verum

end;

hence ( ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 ) by A10, A12; :: thesis: verum

end;

hence ( ( not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y ) or v1 = w1 ) ; :: thesis: verum