let V be RealLinearSpace; :: thesis: for u, u1, v, v1, w, y being VECTOR of V st Gen w,y & u,v,u1,v1 are_DTr_wrt w,y holds
u,v,u # u1,v # v1 are_DTr_wrt w,y
let u, u1, v, v1, w, y be VECTOR of V; :: thesis: ( Gen w,y & u,v,u1,v1 are_DTr_wrt w,y implies u,v,u # u1,v # v1 are_DTr_wrt w,y )
assume that
A1: Gen w,y and
A2: u,v,u1,v1 are_DTr_wrt w,y ; :: thesis: u,v,u # u1,v # v1 are_DTr_wrt w,y
set p = u # u1;
set q = v # v1;
set r = u # v;
set s = u1 # v1;
A3: ( u = v & u1 = v1 implies u # u1,v # v1,u # v,(u # u1) # (v # v1) are_Ort_wrt w,y ) by A1, Lm9;
(u # u1) # (v # v1) = (u # v) # (u1 # v1) by Th6;
then u # v,u1 # v1 // u # v,(u # u1) # (v # v1) by Th12;
then A4: u # v,u1 # v1 '||' u # v,(u # u1) # (v # v1) ;
( u,v,u # v,u1 # v1 are_Ort_wrt w,y & u1,v1,u # v,u1 # v1 are_Ort_wrt w,y ) by A2;
then A5: ( u # v <> u1 # v1 implies ( u1,v1,u # v,(u # u1) # (v # v1) are_Ort_wrt w,y & u,v,u # v,(u # u1) # (v # v1) are_Ort_wrt w,y ) ) by A1, A4, Lm10;

A6: now :: thesis: ( u # v = u1 # v1 implies ( u1,v1,u # v,(u # u1) # (v # v1) are_Ort_wrt w,y & u,v,u # v,(u # u1) # (v # v1) are_Ort_wrt w,y ) )

assume u # v = u1 # v1 ; :: thesis: ( u1,v1,u # v,(u # u1) # (v # v1) are_Ort_wrt w,y & u,v,u # v,(u # u1) # (v # v1) are_Ort_wrt w,y )
then u # v = (u # v) # (u1 # v1)
.= (u # u1) # (v # v1) by Th6 ;
hence ( u1,v1,u # v,(u # u1) # (v # v1) are_Ort_wrt w,y & u,v,u # v,(u # u1) # (v # v1) are_Ort_wrt w,y ) by A1, Lm9; :: thesis: verum

end;

A7: u,v // u1,v1 by A2;
then u1,v1 // u,v by ANALOAF:12;
then u1,v1 // u1 # u,v1 # v by Th14;
then u1,v1 '||' u # u1,v # v1 ;
then A8: ( u = v & u1 <> v1 implies u # u1,v # v1,u # v,(u # u1) # (v # v1) are_Ort_wrt w,y ) by A1, A6, A5, Lm10;
A9: u,v // u # u1,v # v1 by A7, Th14;
then u,v '||' u # u1,v # v1 ;
then ( u <> v implies u # u1,v # v1,u # v,(u # u1) # (v # v1) are_Ort_wrt w,y ) by A1, A6, A5, Lm10;
hence u,v,u # u1,v # v1 are_DTr_wrt w,y by A9, A6, A5, A8, A3; :: thesis: verum