let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V
for a, b, c, d being Element of (DTrSpace V,w,y) st Gen w,y & a,b // c,d holds
a,b // a # c,b # d
let w, y be VECTOR of V; :: thesis: for a, b, c, d being Element of (DTrSpace V,w,y) st Gen w,y & a,b // c,d holds
a,b // a # c,b # d
let a, b, c, d be Element of (DTrSpace V,w,y); :: thesis: ( Gen w,y & a,b // c,d implies a,b // a # c,b # d )
assume that
A1: Gen w,y and
A2: a,b // c,d ; :: thesis: a,b // a # c,b # d
reconsider u = a, v = b, u1 = c, v1 = d as VECTOR of V ;
A3: ( a # c = u # u1 & b # d = v # v1 ) by Def8;
u,v,u1,v1 are_DTr_wrt w,y by A1, A2, Th47;
then u,v,u # u1,v # v1 are_DTr_wrt w,y by A1, Th28;
hence a,b // a # c,b # d by A1, A3, Th47; :: thesis: verum