:: deftheorem Def2 defines are_Ort_wrt ANALMETR:def 2 :
for V being RealLinearSpace
for u, v, w, y being VECTOR of V holds
( u,v are_Ort_wrt w,y iff ex a1, a2, b1, b2 being Real st
( u = (a1 * w) + (a2 * y) & v = (b1 * w) + (b2 * y) & (a1 * b1) + (a2 * b2) = 0 ) );