let V be RealLinearSpace; :: thesis: for u, u1, v, w, y being VECTOR of V st Gen w,y holds
ex t being VECTOR of V st
( u,v,u1,t are_DTr_wrt w,y or u,v,t,u1 are_DTr_wrt w,y )
let u, u1, v, w, y be VECTOR of V; :: thesis: ( Gen w,y implies ex t being VECTOR of V st
( u,v,u1,t are_DTr_wrt w,y or u,v,t,u1 are_DTr_wrt w,y ) )
assume A1: Gen w,y ; :: thesis: ex t being VECTOR of V st
( u,v,u1,t are_DTr_wrt w,y or u,v,t,u1 are_DTr_wrt w,y )
set a = u # v;

per cases ( u = v or u <> v ) ;

suppose A2: u = v ; :: thesis: ex t being VECTOR of V st
( u,v,u1,t are_DTr_wrt w,y or u,v,t,u1 are_DTr_wrt w,y )

A3: u1,u1,u # u,u1 # u1 are_Ort_wrt w,y by A1, Lm5, Lm6;
( u,u // u1,u1 & u,u,u # u,u1 # u1 are_Ort_wrt w,y ) by A1, Lm5, Lm6, ANALOAF:9;
then u,u,u1,u1 are_DTr_wrt w,y by A3;
hence ex t being VECTOR of V st
( u,v,u1,t are_DTr_wrt w,y or u,v,t,u1 are_DTr_wrt w,y ) by A2; :: thesis: verum

end;

suppose A4: u <> v ; :: thesis: ex t being VECTOR of V st
( u,v,u1,t are_DTr_wrt w,y or u,v,t,u1 are_DTr_wrt w,y )

u # v <> u

proof

assume u # v = u ; :: thesis: contradiction
then u # u = u # v ;
hence contradiction by A4, Th7; :: thesis: verum

end;

then u - (u # v) <> 0. V by RLVECT_1:21;
then consider r being Real such that
A5: (u1 - (u # v)) - (r * (u - (u # v))),u - (u # v) are_Ort_wrt w,y by A1, ANALMETR:13;
set b = u1 - (r * (u - (u # v)));
set t = (2 * (u1 - (r * (u - (u # v))))) - u1;
u1 + ((2 * (u1 - (r * (u - (u # v))))) - u1) = (1 + 1) * (u1 - (r * (u - (u # v)))) by RLSUB_2:61
.= (1 * (u1 - (r * (u - (u # v))))) + (1 * (u1 - (r * (u - (u # v))))) by RLVECT_1:def 6
.= (u1 - (r * (u - (u # v)))) + (1 * (u1 - (r * (u - (u # v))))) by RLVECT_1:def 8
.= (u1 - (r * (u - (u # v)))) + (u1 - (r * (u - (u # v)))) by RLVECT_1:def 8 ;
then A6: u1 # ((2 * (u1 - (r * (u - (u # v))))) - u1) = u1 - (r * (u - (u # v))) by Def2;
u1 - (u1 - (r * (u - (u # v)))) = (u1 - u1) + (r * (u - (u # v))) by RLVECT_1:29
.= (0. V) + (r * (u - (u # v))) by RLVECT_1:15
.= r * (u - (u # v)) by RLVECT_1:4 ;
then A7: u1 - ((2 * (u1 - (r * (u - (u # v))))) - u1) = 2 * (r * (u - (u # v))) by A6, Th10
.= (2 * r) * (u - (u # v)) by RLVECT_1:def 7 ;
A8: u1 - ((u # v) + (r * (u - (u # v)))) = (u1 - (r * (u - (u # v)))) - (u # v) by RLVECT_1:27;
then (u1 - (r * (u - (u # v)))) - (u # v),u - (u # v) are_Ort_wrt w,y by A5, RLVECT_1:27;
then (u1 - (r * (u - (u # v)))) - (u # v),u1 - ((2 * (u1 - (r * (u - (u # v))))) - u1) are_Ort_wrt w,y by A7, ANALMETR:7;
then A9: u # v,u1 - (r * (u - (u # v))),(2 * (u1 - (r * (u - (u # v))))) - u1,u1 are_Ort_wrt w,y by ANALMETR:def 3;
then A10: (2 * (u1 - (r * (u - (u # v))))) - u1,u1,u # v,((2 * (u1 - (r * (u - (u # v))))) - u1) # u1 are_Ort_wrt w,y by A6, Lm5;
A11: u - v = 2 * (u - (u # v)) by Th10;
then u1 - ((2 * (u1 - (r * (u - (u # v))))) - u1) = r * (u - v) by A7, RLVECT_1:def 7;
then r * (u - v) = 1 * (u1 - ((2 * (u1 - (r * (u - (u # v))))) - u1)) by RLVECT_1:def 8;
then ( v,u // (2 * (u1 - (r * (u - (u # v))))) - u1,u1 or v,u // u1,(2 * (u1 - (r * (u - (u # v))))) - u1 ) by ANALMETR:14;
then A12: ( u,v // u1,(2 * (u1 - (r * (u - (u # v))))) - u1 or u,v // (2 * (u1 - (r * (u - (u # v))))) - u1,u1 ) by ANALOAF:12;
u # v,u1 - (r * (u - (u # v))),u1,(2 * (u1 - (r * (u - (u # v))))) - u1 are_Ort_wrt w,y by A9, Lm4;
then A13: u1,(2 * (u1 - (r * (u - (u # v))))) - u1,u # v,u1 # ((2 * (u1 - (r * (u - (u # v))))) - u1) are_Ort_wrt w,y by A6, Lm5;
(u1 - (r * (u - (u # v)))) - (u # v) = (u1 - (u # v)) - (r * (u - (u # v))) by A8, RLVECT_1:27;
then (u1 - (r * (u - (u # v)))) - (u # v),u - v are_Ort_wrt w,y by A5, A11, ANALMETR:7;
then u # v,u1 - (r * (u - (u # v))),v,u are_Ort_wrt w,y by ANALMETR:def 3;
then u # v,u1 - (r * (u - (u # v))),u,v are_Ort_wrt w,y by Lm4;
then u,v,u # v,u1 # ((2 * (u1 - (r * (u - (u # v))))) - u1) are_Ort_wrt w,y by A6, Lm5;
then ( u,v,u1,(2 * (u1 - (r * (u - (u # v))))) - u1 are_DTr_wrt w,y or u,v,(2 * (u1 - (r * (u - (u # v))))) - u1,u1 are_DTr_wrt w,y ) by A13, A10, A12;
hence ex t being VECTOR of V st
( u,v,u1,t are_DTr_wrt w,y or u,v,t,u1 are_DTr_wrt w,y ) ; :: thesis: verum

end;

end;