let V be RealLinearSpace; 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; ( 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 )
; v1 = v2
now ( u,u1,v2,v are_DTr_wrt w,y implies v1 = v2 )assume
u,
u1,
v2,
v are_DTr_wrt w,
y
;
v1 = v2then 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;
verum end;
hence
v1 = v2
by A1, A2, A3, Th24; verum