let V be RealLinearSpace; :: thesis: for w, y, u, v, u1 being VECTOR of V st Gen w,y holds
( u,v,u1,u1 are_Ort_wrt w,y & u1,u1,u,v are_Ort_wrt w,y )
let w, y, u, v, u1 be VECTOR of V; :: thesis: ( Gen w,y implies ( u,v,u1,u1 are_Ort_wrt w,y & u1,u1,u,v are_Ort_wrt w,y ) )
A1: u1 - u1 = 0. V by RLVECT_1:15;
assume Gen w,y ; :: thesis: ( u,v,u1,u1 are_Ort_wrt w,y & u1,u1,u,v are_Ort_wrt w,y )
then v - u,u1 - u1 are_Ort_wrt w,y by A1, ANALMETR:5;
hence u,v,u1,u1 are_Ort_wrt w,y by ANALMETR:def 3; :: thesis: u1,u1,u,v are_Ort_wrt w,y
hence u1,u1,u,v are_Ort_wrt w,y by Lm5; :: thesis: verum