let V be RealLinearSpace; :: thesis: for u, u1, v, v1, v2, w, y being VECTOR of V st Gen w,y & u <> u1 & u,u1,v,v1 are_DTr_wrt w,y & ( u,u1,v,v2 are_DTr_wrt w,y or u,u1,v2,v are_DTr_wrt w,y ) holds
v1 = v2
let u, u1, v, v1, v2, w, y be VECTOR of V; :: thesis: ( Gen w,y & u <> u1 & u,u1,v,v1 are_DTr_wrt w,y & ( u,u1,v,v2 are_DTr_wrt w,y or u,u1,v2,v are_DTr_wrt w,y ) implies v1 = v2 )
assume that
A1: Gen w,y and
A2: ( u <> u1 & u,u1,v,v1 are_DTr_wrt w,y ) and
A3: ( u,u1,v,v2 are_DTr_wrt w,y or u,u1,v2,v are_DTr_wrt w,y ) ; :: thesis: v1 = v2

now :: thesis: ( u,u1,v2,v are_DTr_wrt w,y implies v1 = v2 )

assume u,u1,v2,v are_DTr_wrt w,y ; :: thesis: v1 = v2
then A4: v2,v,v,v1 are_DTr_wrt w,y by A1, A2, Th19;
then v = v2 by A1, Th18;
hence v1 = v2 by A1, A4, Th18; :: thesis: verum

end;

hence v1 = v2 by A1, A2, A3, Th24; :: thesis: verum