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