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