let V be RealLinearSpace; :: thesis: for u, v, u1, 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, v, u1, v1, w, y be VECTOR of V; :: thesis: ( 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
; :: thesis: v,u,v1,u1 are_DTr_wrt w,y
then
u,v // u1,v1
by Def3;
then A2:
v,u // v1,u1
by ANALOAF:21;
A3:
now let u,
u',
v,
v' be
VECTOR of
V;
:: thesis: ( u,u',v,v' are_Ort_wrt w,y implies u',u,v,v' are_Ort_wrt w,y )assume
u,
u',
v,
v' are_Ort_wrt w,
y
;
:: thesis: u',u,v,v' are_Ort_wrt w,ythen
v,
v',
u,
u' are_Ort_wrt w,
y
by Lm5;
then
v,
v',
u',
u are_Ort_wrt w,
y
by Lm4;
hence
u',
u,
v,
v' are_Ort_wrt w,
y
by Lm5;
:: thesis: verum end;
u1,v1,u # v,u1 # v1 are_Ort_wrt w,y
by A1, Def3;
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, Def3;
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, Def3; :: thesis: verum