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