let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V
for a, b, c, d1, d2 being Element of (DTrSpace (V,w,y)) st Gen w,y & a,b // c,d1 & a,b // c,d2 & not a = b holds
d1 = d2
let w, y be VECTOR of V; :: thesis: for a, b, c, d1, d2 being Element of (DTrSpace (V,w,y)) st Gen w,y & a,b // c,d1 & a,b // c,d2 & not a = b holds
d1 = d2
let a, b, c, d1, d2 be Element of (DTrSpace (V,w,y)); :: thesis: ( Gen w,y & a,b // c,d1 & a,b // c,d2 & not a = b implies d1 = d2 )
assume that
A1: Gen w,y and
A2: ( a,b // c,d1 & a,b // c,d2 ) ; :: thesis: ( a = b or d1 = d2 )
reconsider u = a, v = b, u1 = c, v1 = d1, v2 = d2 as VECTOR of V ;
( u,v,u1,v1 are_DTr_wrt w,y & u,v,u1,v2 are_DTr_wrt w,y ) by A2, Th44;
hence ( a = b or d1 = d2 ) by A1, Th24; :: thesis: verum