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