let V be RealLinearSpace; :: thesis: for w, y, u, v, u1, v1 being VECTOR of V st Gen w,y & u,v,u1,v1 are_DTr_wrt w,y holds
u1,v1,u,v are_DTr_wrt w,y
let w, y, u, v, u1, v1 be VECTOR of V; :: thesis: ( Gen w,y & u,v,u1,v1 are_DTr_wrt w,y implies u1,v1,u,v are_DTr_wrt w,y )
assume that
A1: Gen w,y and
A2: u,v,u1,v1 are_DTr_wrt w,y ; :: thesis: u1,v1,u,v are_DTr_wrt w,y
X: ( u,v // u1,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, Def3;
Y: u1,v1 // u,v by X, ANALOAF:21;
( u1,v1,u1 # v1,u # v are_Ort_wrt w,y & u,v,u1 # v1,u # v are_Ort_wrt w,y ) by A1, Lm4, X;
hence u1,v1,u,v are_DTr_wrt w,y by Def3, Y; :: thesis: verum