let V be RealLinearSpace; for u, u1, u2, v, v1, v2, w, y being VECTOR of V st Gen w,y & u,v,u1,v1 are_DTr_wrt w,y & u,v,u2,v2 are_DTr_wrt w,y & u <> v holds
u1,v1,u2,v2 are_DTr_wrt w,y
let u, u1, u2, v, v1, v2, w, y be VECTOR of V; ( Gen w,y & u,v,u1,v1 are_DTr_wrt w,y & u,v,u2,v2 are_DTr_wrt w,y & u <> v implies u1,v1,u2,v2 are_DTr_wrt w,y )
assume that
A1:
Gen w,y
and
A2:
u,v,u1,v1 are_DTr_wrt w,y
and
A3:
u,v,u2,v2 are_DTr_wrt w,y
and
A4:
u <> v
; u1,v1,u2,v2 are_DTr_wrt w,y
set a = u1 # v1;
set b = u2 # v2;
( u,v,u # v,u1 # v1 are_Ort_wrt w,y & u,v,u # v,u2 # v2 are_Ort_wrt w,y )
by A2, A3;
then A5:
u,v,u1 # v1,u2 # v2 are_Ort_wrt w,y
by A1, Lm7;
A6:
u,v // u2,v2
by A3;
then
u,v '||' u2,v2
;
then A7:
u2,v2,u1 # v1,u2 # v2 are_Ort_wrt w,y
by A1, A4, A5, Lm10;
A8:
u,v // u1,v1
by A2;
then
u,v '||' u1,v1
;
then A9:
u1,v1,u1 # v1,u2 # v2 are_Ort_wrt w,y
by A1, A4, A5, Lm10;
u1,v1 // u2,v2
by A4, A8, A6, ANALOAF:11;
hence
u1,v1,u2,v2 are_DTr_wrt w,y
by A9, A7; verum