let V be RealLinearSpace; :: thesis: for w, y, u, v, u1 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 w, y, u, v, u1 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;

A2: now

assume A3: 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,u // u1,u1 & u # u,u1 # u1,u,u are_Ort_wrt w,y & u # u,u1 # u1,u1,u1 are_Ort_wrt w,y ) by A1, Lm5, ANALOAF:18;
then ( u,u // u1,u1 & u,u,u # u,u1 # u1 are_Ort_wrt w,y & u1,u1,u # u,u1 # u1 are_Ort_wrt w,y ) by A1, Lm4A;
then u,u,u1,u1 are_DTr_wrt w,y by Def3;
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 A3; :: thesis: verum

end;

now

assume 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, Th9; :: thesis: verum

end;

then u - (u # v) <> 0. V by RLVECT_1:35;
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:17;
set b = u1 - (r * (u - (u # v)));
set t = (2 * (u1 - (r * (u - (u # v))))) - u1;
A6: u - v = 2 * (u - (u # v)) by Th12;
A7: u1 # ((2 * (u1 - (r * (u - (u # v))))) - u1) = u1 - (r * (u - (u # v)))

proof

u1 + ((2 * (u1 - (r * (u - (u # v))))) - u1) = (1 + 1) * (u1 - (r * (u - (u # v)))) by RLSUB_2:78
.= (1 * (u1 - (r * (u - (u # v))))) + (1 * (u1 - (r * (u - (u # v))))) by RLVECT_1:def 9
.= (u1 - (r * (u - (u # v)))) + (1 * (u1 - (r * (u - (u # v))))) by RLVECT_1:def 9
.= (u1 - (r * (u - (u # v)))) + (u1 - (r * (u - (u # v)))) by RLVECT_1:def 9 ;
hence u1 # ((2 * (u1 - (r * (u - (u # v))))) - u1) = u1 - (r * (u - (u # v))) by Def2; :: thesis: verum

end;

A8: u1 - ((u # v) + (r * (u - (u # v)))) = (u1 - (r * (u - (u # v)))) - (u # v) by RLVECT_1:41;
then A9: (u1 - (r * (u - (u # v)))) - (u # v) = (u1 - (u # v)) - (r * (u - (u # v))) by RLVECT_1:41;
A10: (u1 - (r * (u - (u # v)))) - (u # v),u - (u # v) are_Ort_wrt w,y by A5, A8, RLVECT_1:41;
(u1 - (r * (u - (u # v)))) - (u # v),u - v are_Ort_wrt w,y by A5, A6, A9, ANALMETR:11;
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 A1, Lm4;
then A11: u,v,u # v,u1 # ((2 * (u1 - (r * (u - (u # v))))) - u1) are_Ort_wrt w,y by A1, A7, Lm4A;
u1 - (u1 - (r * (u - (u # v)))) = (u1 - u1) + (r * (u - (u # v))) by RLVECT_1:43
.= (0. V) + (r * (u - (u # v))) by RLVECT_1:28
.= r * (u - (u # v)) by RLVECT_1:10 ;
then A12: u1 - ((2 * (u1 - (r * (u - (u # v))))) - u1) = 2 * (r * (u - (u # v))) by A7, Th12
.= (2 * r) * (u - (u # v)) by RLVECT_1:def 9 ;
then A13: u1 - ((2 * (u1 - (r * (u - (u # v))))) - u1) = r * (u - v) by A6, RLVECT_1:def 9;

A14: now

assume A15: r = 0 ; :: 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 )
A16: ( u1 - (r * (u - (u # v))) = u1 & (2 * (u1 - (r * (u - (u # v))))) - u1 = u1 )

proof

thus u1 - (r * (u - (u # v))) = u1 - (0. V) by A15, RLVECT_1:23
.= u1 by RLVECT_1:26 ; :: thesis: (2 * (u1 - (r * (u - (u # v))))) - u1 = u1
hence (2 * (u1 - (r * (u - (u # v))))) - u1 = ((1 + 1) * u1) - u1
.= ((1 * u1) + (1 * u1)) - u1 by RLVECT_1:def 9
.= (u1 + (1 * u1)) - u1 by RLVECT_1:def 9
.= (u1 + u1) - u1 by RLVECT_1:def 9
.= u1 by RLSUB_2:78 ;
:: thesis: verum

end;

( u,v // u1,(2 * (u1 - (r * (u - (u # v))))) - u1 & u1,(2 * (u1 - (r * (u - (u # v))))) - u1,u # v,u1 # ((2 * (u1 - (r * (u - (u # v))))) - u1) are_Ort_wrt w,y )

proof

thus u,v // u1,(2 * (u1 - (r * (u - (u # v))))) - u1 by A16, ANALOAF:18; :: thesis: u1,(2 * (u1 - (r * (u - (u # v))))) - u1,u # v,u1 # ((2 * (u1 - (r * (u - (u # v))))) - u1) are_Ort_wrt w,y
u # v,u1 - (r * (u - (u # v))),u1,(2 * (u1 - (r * (u - (u # v))))) - u1 are_Ort_wrt w,y by A1, A16, Lm5;
hence u1,(2 * (u1 - (r * (u - (u # v))))) - u1,u # v,u1 # ((2 * (u1 - (r * (u - (u # v))))) - u1) are_Ort_wrt w,y by A1, A7, Lm4A; :: thesis: verum

end;

then u,v,u1,(2 * (u1 - (r * (u - (u # v))))) - u1 are_DTr_wrt w,y by A11, Def3;
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;

now

assume r <> 0 ; :: thesis: ( 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 )
(u1 - (r * (u - (u # v)))) - (u # v),u1 - ((2 * (u1 - (r * (u - (u # v))))) - u1) are_Ort_wrt w,y by A10, A12, ANALMETR:11;
then A17: 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 u # v,u1 - (r * (u - (u # v))),u1,(2 * (u1 - (r * (u - (u # v))))) - u1 are_Ort_wrt w,y by A1, Lm4;
then A18: u1,(2 * (u1 - (r * (u - (u # v))))) - u1,u # v,u1 # ((2 * (u1 - (r * (u - (u # v))))) - u1) are_Ort_wrt w,y by A1, A7, Lm4A;
A19: (2 * (u1 - (r * (u - (u # v))))) - u1,u1,u # v,((2 * (u1 - (r * (u - (u # v))))) - u1) # u1 are_Ort_wrt w,y by A1, A7, A17, Lm4A;
r * (u - v) = 1 * (u1 - ((2 * (u1 - (r * (u - (u # v))))) - u1)) by A13, RLVECT_1:def 9;
then ( v,u // (2 * (u1 - (r * (u - (u # v))))) - u1,u1 or v,u // u1,(2 * (u1 - (r * (u - (u # v))))) - u1 ) by ANALMETR:18;
then ( u,v // u1,(2 * (u1 - (r * (u - (u # v))))) - u1 or u,v // (2 * (u1 - (r * (u - (u # v))))) - u1,u1 ) by ANALOAF:21;
hence ( 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 A11, A18, A19, Def3; :: thesis: verum

end;

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 A14; :: thesis: verum

end;

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