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, Th30
.= PProJ (w,y,(u - u9),(v1 + v1)) by A5, Def2
.= (PProJ (w,y,(u - u9),v1)) + (PProJ (w,y,(u - u9),v1)) by A1, Th30 ;
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, Th36;
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 3
.= ((((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 3
.= (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 3
.= (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 6 ;
( 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, Th36;
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 3
.= ((((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 3
.= (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 3
.= (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 6
.= (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