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 & 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 A4; :: 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 )
A5: Orte x,y,u, Orte x,y,v // u,w by A4, 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 A6: Orte x,y,v1, Orte x,y,w1 // u,v by Def3;

now

assume A7: 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, A6, A7, 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, A5, Th13, ANALOAF:20;
then consider a, b being Real such that
A8: ( a * (w - u) = b * ((Orte x,y,w) - (Orte x,y,u)) & ( 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)) & ( a <> 0 or b <> 0 ) ) by A1, A8, Th11;
then A9: ( a * (((pr1 x,y,(w - u)) * x) + ((pr2 x,y,(w - u)) * y)) = b * (Orte x,y,(w - u)) & ( a <> 0 or b <> 0 ) ) by A1, Lm5;

A10: now

assume A11: 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 )
A12: pr2 x,y,(w - u) <> 0

proof

assume A13: 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 A9, 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 A11, XCMPLX_1:6;
then w - u = (0 * x) + (0 * y) by A1, A13, 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 A9, 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 A11, 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 ((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)) & pr2 x,y,(w - u) = ((a " ) * b) * (- (pr1 x,y,(w - u))) ) by A1, Lm3;
then A14: pr2 x,y,(w - u) = - (((a " ) * b) * (((a " ) * b) * (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)))
.= ((pr2 x,y,(w - u)) " ) * (((a " ) * b) * (((a " ) * b) * (pr2 x,y,(w - u)))) by A14 ;
then - 1 = (((pr2 x,y,(w - u)) " ) * (pr2 x,y,(w - u))) * (((a " ) * b) * ((a " ) * b)) by A12, XCMPLX_0:def 7;
then - 1 = 1 * (((a " ) * b) * ((a " ) * b)) by A12, 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 A15: 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 )
A16: pr2 x,y,(w - u) <> 0

proof

assume A17: 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 A9, 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 A15, XCMPLX_1:6;
then w - u = (0 * x) + ((- 0 ) * y) by A1, A17, 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 A9, 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 A15, 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 ((((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) * (pr1 x,y,(w - u)) = pr2 x,y,(w - u) & ((b " ) * a) * (pr2 x,y,(w - u)) = - (pr1 x,y,(w - u)) ) by A1, Lm3;
then A18: pr2 x,y,(w - u) = ((b " ) * a) * (- (((b " ) * a) * (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)))
.= ((pr2 x,y,(w - u)) " ) * (((b " ) * a) * (((b " ) * a) * (pr2 x,y,(w - u)))) by A18 ;
then - 1 = (((pr2 x,y,(w - u)) " ) * (pr2 x,y,(w - u))) * (((b " ) * a) * ((b " ) * a)) by A16, XCMPLX_0:def 7;
then - 1 = 1 * (((b " ) * a) * ((b " ) * a)) by A16, 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 A8, A10; :: 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