let V be RealLinearSpace; :: thesis: for u, v, w, y being VECTOR of V st u,v,v,u are_DTr_wrt w,y holds
u = v
let u, v, w, y be VECTOR of V; :: thesis: ( u,v,v,u are_DTr_wrt w,y implies u = v )
assume u,v,v,u are_DTr_wrt w,y ; :: thesis: u = v
then u,v // v,u by Def3;
hence u = v by ANALOAF:19; :: thesis: verum