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