let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V
for a, b, c, d, a1, b1, c1, d1, p, q 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 a, b, c, d, a1, b1, c1, d1, p, q 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 a, b, c, d, a1, b1, c1, d1, p, q 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 & p <> q ) and
A2: ( p,q // a,a1 & p,q // b,b1 ) and
A3: ( p,q // c,c1 & p,q // d,d1 ) and
A4: a,b // c,d ; :: thesis: a1,b1 // c1,d1
reconsider u = p, u9 = q, u1 = a, u2 = b, v1 = c, v2 = d, t1 = a1, t2 = b1, w1 = c1, w2 = d1 as VECTOR of V ;
A5: ( u,u9,v1,w1 are_DTr_wrt w,y & u,u9,v2,w2 are_DTr_wrt w,y ) by A3, Th44;
A6: u1,u2,v1,v2 are_DTr_wrt w,y by A4, Th44;
( u,u9,u1,t1 are_DTr_wrt w,y & u,u9,u2,t2 are_DTr_wrt w,y ) by A2, Th44;
then t1,t2,w1,w2 are_DTr_wrt w,y by A1, A5, A6, Th41;
hence a1,b1 // c1,d1 by Th44; :: thesis: verum