let V be RealLinearSpace; for w, y being VECTOR of V st Gen w,y holds
for u, v being VECTOR of V holds
( u,v are_Ort_wrt w,y iff PProJ (w,y,u,v) = 0 )
let w, y be VECTOR of V; ( Gen w,y implies for u, v being VECTOR of V holds
( u,v are_Ort_wrt w,y iff PProJ (w,y,u,v) = 0 ) )
assume A1:
Gen w,y
; for u, v being VECTOR of V holds
( u,v are_Ort_wrt w,y iff PProJ (w,y,u,v) = 0 )
let u, v be VECTOR of V; ( u,v are_Ort_wrt w,y iff PProJ (w,y,u,v) = 0 )
set a1 = pr1 (w,y,u);
set a2 = pr2 (w,y,u);
set b1 = pr1 (w,y,v);
set b2 = pr2 (w,y,v);
( u = ((pr1 (w,y,u)) * w) + ((pr2 (w,y,u)) * y) & v = ((pr1 (w,y,v)) * w) + ((pr2 (w,y,v)) * y) )
by A1, Lm15;
hence
( u,v are_Ort_wrt w,y iff PProJ (w,y,u,v) = 0 )
by A1, ANALMETR:1, ANALMETR:def 2; verum