let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V st Gen w,y holds
for u, v, u1, v1 being VECTOR of V holds
( u,v,u1,v1 are_Ort_wrt w,y iff PProJ w,y,(v - u),(v1 - u1) = 0 )
let w, y be VECTOR of V; :: thesis: ( Gen w,y implies for u, v, u1, v1 being VECTOR of V holds
( u,v,u1,v1 are_Ort_wrt w,y iff PProJ w,y,(v - u),(v1 - u1) = 0 ) )
assume A1: Gen w,y ; :: thesis: for u, v, u1, v1 being VECTOR of V holds
( u,v,u1,v1 are_Ort_wrt w,y iff PProJ w,y,(v - u),(v1 - u1) = 0 )
let u, v, u1, v1 be VECTOR of V; :: thesis: ( u,v,u1,v1 are_Ort_wrt w,y iff PProJ w,y,(v - u),(v1 - u1) = 0 )
( u,v,u1,v1 are_Ort_wrt w,y iff v - u,v1 - u1 are_Ort_wrt w,y ) by ANALMETR:def 3;
hence ( u,v,u1,v1 are_Ort_wrt w,y iff PProJ w,y,(v - u),(v1 - u1) = 0 ) by A1, Th34; :: thesis: verum