let V be RealLinearSpace; for u, u1, v, v1, w, y being VECTOR of V st u,v,u1,v1 are_DTr_wrt w,y holds
v,u,v1,u1 are_DTr_wrt w,y
let u, u1, v, v1, w, y be VECTOR of V; ( u,v,u1,v1 are_DTr_wrt w,y implies v,u,v1,u1 are_DTr_wrt w,y )
assume A1:
u,v,u1,v1 are_DTr_wrt w,y
; v,u,v1,u1 are_DTr_wrt w,y
then
u,v // u1,v1
;
then A2:
v,u // v1,u1
by ANALOAF:12;
A3:
now for u, u9, v, v9 being VECTOR of V st u,u9,v,v9 are_Ort_wrt w,y holds
u9,u,v,v9 are_Ort_wrt w,ylet u,
u9,
v,
v9 be
VECTOR of
V;
( u,u9,v,v9 are_Ort_wrt w,y implies u9,u,v,v9 are_Ort_wrt w,y )assume
u,
u9,
v,
v9 are_Ort_wrt w,
y
;
u9,u,v,v9 are_Ort_wrt w,ythen
v,
v9,
u,
u9 are_Ort_wrt w,
y
by Lm5;
then
v,
v9,
u9,
u are_Ort_wrt w,
y
by Lm4;
hence
u9,
u,
v,
v9 are_Ort_wrt w,
y
by Lm5;
verum end;
u1,v1,u # v,u1 # v1 are_Ort_wrt w,y
by A1;
then A4:
v1,u1,v # u,v1 # u1 are_Ort_wrt w,y
by A3;
u,v,u # v,u1 # v1 are_Ort_wrt w,y
by A1;
then
v,u,v # u,v1 # u1 are_Ort_wrt w,y
by A3;
hence
v,u,v1,u1 are_DTr_wrt w,y
by A2, A4; verum