let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V st Gen w,y holds
for u, u9, u1, u2, v1, t1, t2, w1 being VECTOR of V st u <> u9 & u,u9,u1,t1 are_DTr_wrt w,y & u,u9,u2,t2 are_DTr_wrt w,y & u,u9,v1,w1 are_DTr_wrt w,y & v1 = u1 # u2 holds
w1 = t1 # t2
let w, y be VECTOR of V; :: thesis: ( Gen w,y implies for u, u9, u1, u2, v1, t1, t2, w1 being VECTOR of V st u <> u9 & u,u9,u1,t1 are_DTr_wrt w,y & u,u9,u2,t2 are_DTr_wrt w,y & u,u9,v1,w1 are_DTr_wrt w,y & v1 = u1 # u2 holds
w1 = t1 # t2 )
assume A1: Gen w,y ; :: thesis: for u, u9, u1, u2, v1, t1, t2, w1 being VECTOR of V st u <> u9 & u,u9,u1,t1 are_DTr_wrt w,y & u,u9,u2,t2 are_DTr_wrt w,y & u,u9,v1,w1 are_DTr_wrt w,y & v1 = u1 # u2 holds
w1 = t1 # t2
let u, u9, u1, u2, v1, t1, t2, w1 be VECTOR of V; :: thesis: ( u <> u9 & u,u9,u1,t1 are_DTr_wrt w,y & u,u9,u2,t2 are_DTr_wrt w,y & u,u9,v1,w1 are_DTr_wrt w,y & v1 = u1 # u2 implies w1 = t1 # t2 )
assume that
A2: u <> u9 and
A3: ( u,u9,u1,t1 are_DTr_wrt w,y & u,u9,u2,t2 are_DTr_wrt w,y ) and
A4: u,u9,v1,w1 are_DTr_wrt w,y and
A5: v1 = u1 # u2 ; :: thesis: w1 = t1 # t2
set G = PProJ w,y,(u - u9),(u + u9);
set H = PProJ w,y,(u - u9),u1;
set W = PProJ w,y,(u - u9),u2;
set I = PProJ w,y,(u - u9),v1;
set N = PProJ w,y,(u - u9),(u - u9);
set A1 = ((PProJ w,y,(u - u9),(u + u9)) - (2 * (PProJ w,y,(u - u9),u1))) * ((PProJ w,y,(u - u9),(u - u9)) " );
set A2 = ((PProJ w,y,(u - u9),(u + u9)) - (2 * (PProJ w,y,(u - u9),u2))) * ((PProJ w,y,(u - u9),(u - u9)) " );
set A3 = ((PProJ w,y,(u - u9),(u + u9)) - (2 * (PProJ w,y,(u - u9),v1))) * ((PProJ w,y,(u - u9),(u - u9)) " );
A6: (PProJ w,y,(u - u9),u1) + (PProJ w,y,(u - u9),u2) = PProJ w,y,(u - u9),(u1 + u2) by A1, Th32
.= PProJ w,y,(u - u9),(v1 + v1) by A5, Def2
.= (PProJ w,y,(u - u9),v1) + (PProJ w,y,(u - u9),v1) by A1, Th32 ;
v1 + ((((PProJ w,y,(u - u9),(u + u9)) - (2 * (PProJ w,y,(u - u9),v1))) * ((PProJ w,y,(u - u9),(u - u9)) " )) * (u - u9)) = w1 by A1, A2, A4, Th38;
then A7: w1 + w1 = ((((PProJ w,y,(u - u9),(u + u9)) - (2 * (PProJ w,y,(u - u9),v1))) * ((PProJ w,y,(u - u9),(u - u9)) " )) * (u - u9)) + (v1 + (v1 + ((((PProJ w,y,(u - u9),(u + u9)) - (2 * (PProJ w,y,(u - u9),v1))) * ((PProJ w,y,(u - u9),(u - u9)) " )) * (u - u9)))) by RLVECT_1:def 6
.= ((((PProJ w,y,(u - u9),(u + u9)) - (2 * (PProJ w,y,(u - u9),v1))) * ((PProJ w,y,(u - u9),(u - u9)) " )) * (u - u9)) + ((v1 + v1) + ((((PProJ w,y,(u - u9),(u + u9)) - (2 * (PProJ w,y,(u - u9),v1))) * ((PProJ w,y,(u - u9),(u - u9)) " )) * (u - u9))) by RLVECT_1:def 6
.= (v1 + v1) + (((((PProJ w,y,(u - u9),(u + u9)) - (2 * (PProJ w,y,(u - u9),v1))) * ((PProJ w,y,(u - u9),(u - u9)) " )) * (u - u9)) + ((((PProJ w,y,(u - u9),(u + u9)) - (2 * (PProJ w,y,(u - u9),v1))) * ((PProJ w,y,(u - u9),(u - u9)) " )) * (u - u9))) by RLVECT_1:def 6
.= (v1 + v1) + (((((PProJ w,y,(u - u9),(u + u9)) - (2 * (PProJ w,y,(u - u9),v1))) * ((PProJ w,y,(u - u9),(u - u9)) " )) + (((PProJ w,y,(u - u9),(u + u9)) - (2 * (PProJ w,y,(u - u9),v1))) * ((PProJ w,y,(u - u9),(u - u9)) " ))) * (u - u9)) by RLVECT_1:def 9 ;
( u1 + ((((PProJ w,y,(u - u9),(u + u9)) - (2 * (PProJ w,y,(u - u9),u1))) * ((PProJ w,y,(u - u9),(u - u9)) " )) * (u - u9)) = t1 & u2 + ((((PProJ w,y,(u - u9),(u + u9)) - (2 * (PProJ w,y,(u - u9),u2))) * ((PProJ w,y,(u - u9),(u - u9)) " )) * (u - u9)) = t2 ) by A1, A2, A3, Th38;
then A8: t1 + t2 = ((((PProJ w,y,(u - u9),(u + u9)) - (2 * (PProJ w,y,(u - u9),u1))) * ((PProJ w,y,(u - u9),(u - u9)) " )) * (u - u9)) + (u1 + (u2 + ((((PProJ w,y,(u - u9),(u + u9)) - (2 * (PProJ w,y,(u - u9),u2))) * ((PProJ w,y,(u - u9),(u - u9)) " )) * (u - u9)))) by RLVECT_1:def 6
.= ((((PProJ w,y,(u - u9),(u + u9)) - (2 * (PProJ w,y,(u - u9),u1))) * ((PProJ w,y,(u - u9),(u - u9)) " )) * (u - u9)) + ((u1 + u2) + ((((PProJ w,y,(u - u9),(u + u9)) - (2 * (PProJ w,y,(u - u9),u2))) * ((PProJ w,y,(u - u9),(u - u9)) " )) * (u - u9))) by RLVECT_1:def 6
.= (u1 + u2) + (((((PProJ w,y,(u - u9),(u + u9)) - (2 * (PProJ w,y,(u - u9),u1))) * ((PProJ w,y,(u - u9),(u - u9)) " )) * (u - u9)) + ((((PProJ w,y,(u - u9),(u + u9)) - (2 * (PProJ w,y,(u - u9),u2))) * ((PProJ w,y,(u - u9),(u - u9)) " )) * (u - u9))) by RLVECT_1:def 6
.= (u1 + u2) + (((((PProJ w,y,(u - u9),(u + u9)) - (2 * (PProJ w,y,(u - u9),u1))) * ((PProJ w,y,(u - u9),(u - u9)) " )) + (((PProJ w,y,(u - u9),(u + u9)) - (2 * (PProJ w,y,(u - u9),u2))) * ((PProJ w,y,(u - u9),(u - u9)) " ))) * (u - u9)) by RLVECT_1:def 9
.= (v1 + v1) + (((((PProJ w,y,(u - u9),(u + u9)) - (2 * (PProJ w,y,(u - u9),u1))) * ((PProJ w,y,(u - u9),(u - u9)) " )) + (((PProJ w,y,(u - u9),(u + u9)) - (2 * (PProJ w,y,(u - u9),u2))) * ((PProJ w,y,(u - u9),(u - u9)) " ))) * (u - u9)) by A5, Def2 ;
set vv = ((PProJ w,y,(u - u9),(u + u9)) - (2 * (PProJ w,y,(u - u9),v1))) + ((PProJ w,y,(u - u9),(u + u9)) - (2 * (PProJ w,y,(u - u9),v1)));
(((PProJ w,y,(u - u9),(u + u9)) - (2 * (PProJ w,y,(u - u9),u1))) * ((PProJ w,y,(u - u9),(u - u9)) " )) + (((PProJ w,y,(u - u9),(u + u9)) - (2 * (PProJ w,y,(u - u9),u2))) * ((PProJ w,y,(u - u9),(u - u9)) " )) = (((PProJ w,y,(u - u9),(u + u9)) - (2 * (PProJ w,y,(u - u9),u1))) + ((PProJ w,y,(u - u9),(u + u9)) - (2 * (PProJ w,y,(u - u9),u2)))) * ((PProJ w,y,(u - u9),(u - u9)) " )
.= (((PProJ w,y,(u - u9),(u + u9)) - (2 * (PProJ w,y,(u - u9),v1))) + ((PProJ w,y,(u - u9),(u + u9)) - (2 * (PProJ w,y,(u - u9),v1)))) * ((PProJ w,y,(u - u9),(u - u9)) " ) by A6
.= (((PProJ w,y,(u - u9),(u + u9)) - (2 * (PProJ w,y,(u - u9),v1))) * ((PProJ w,y,(u - u9),(u - u9)) " )) + (((PProJ w,y,(u - u9),(u + u9)) - (2 * (PProJ w,y,(u - u9),v1))) * ((PProJ w,y,(u - u9),(u - u9)) " )) ;
hence w1 = t1 # t2 by A8, A7, Def2; :: thesis: verum