let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V
for p, q, a, a1, b, b1, c, c1, d, d1 being Element of (DTrSpace V,w,y) st Gen w,y & p <> q & p,q // a,a1 & p,q // b,b1 & p,q // c,c1 & p,q // d,d1 & a,b // c,d holds
a1,b1 // c1,d1
let w, y be VECTOR of V; :: thesis: for p, q, a, a1, b, b1, c, c1, d, d1 being Element of (DTrSpace V,w,y) st Gen w,y & p <> q & p,q // a,a1 & p,q // b,b1 & p,q // c,c1 & p,q // d,d1 & a,b // c,d holds
a1,b1 // c1,d1
let p, q, a, a1, b, b1, c, c1, d, d1 be Element of (DTrSpace V,w,y); :: thesis: ( Gen w,y & p <> q & p,q // a,a1 & p,q // b,b1 & p,q // c,c1 & p,q // d,d1 & a,b // c,d implies a1,b1 // c1,d1 )
assume that
A1: Gen w,y and
Y: p <> q and
X: ( p,q // a,a1 & p,q // b,b1 & p,q // c,c1 & p,q // d,d1 ) and
A2: a,b // c,d ; :: thesis: a1,b1 // c1,d1
reconsider u = p, u' = q, u1 = a, u2 = b, v1 = c, v2 = d, t1 = a1, t2 = b1, w1 = c1, w2 = d1 as VECTOR of V ;
( u,u',u1,t1 are_DTr_wrt w,y & u,u',u2,t2 are_DTr_wrt w,y & u,u',v1,w1 are_DTr_wrt w,y & u,u',v2,w2 are_DTr_wrt w,y & u1,u2,v1,v2 are_DTr_wrt w,y ) by A1, A2, Th47, X;
then t1,t2,w1,w2 are_DTr_wrt w,y by A1, Th43, Y;
hence a1,b1 // c1,d1 by A1, Th47; :: thesis: verum