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_Ort_wrt w,y holds
u,v,v1,u1 are_Ort_wrt w,y
let w, y, u, v, u1, v1 be VECTOR of V; :: thesis: ( Gen w,y & u,v,u1,v1 are_Ort_wrt w,y implies u,v,v1,u1 are_Ort_wrt w,y )
assume that
Gen w,y and
A1: u,v,u1,v1 are_Ort_wrt w,y ; :: thesis: u,v,v1,u1 are_Ort_wrt w,y
A2: v - u,v1 - u1 are_Ort_wrt w,y by A1, ANALMETR:def 3;
A3: v - u,(- 1) * (v1 - u1) are_Ort_wrt w,y by A2, ANALMETR:11;
(- 1) * (v1 - u1) = - (v1 - u1) by RLVECT_1:29
.= u1 - v1 by RLVECT_1:47 ;
hence u,v,v1,u1 are_Ort_wrt w,y by A3, ANALMETR:def 3; :: thesis: verum