let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V st Gen w,y holds
for u, v being VECTOR of V st u <> v holds
PProJ (w,y,(u - v),(u - v)) <> 0
let w, y be VECTOR of V; :: thesis: ( Gen w,y implies for u, v being VECTOR of V st u <> v holds
PProJ (w,y,(u - v),(u - v)) <> 0 )
assume A1: Gen w,y ; :: thesis: for u, v being VECTOR of V st u <> v holds
PProJ (w,y,(u - v),(u - v)) <> 0
let u, v be VECTOR of V; :: thesis: ( u <> v implies PProJ (w,y,(u - v),(u - v)) <> 0 )
assume A2: u <> v ; :: thesis: PProJ (w,y,(u - v),(u - v)) <> 0
assume PProJ (w,y,(u - v),(u - v)) = 0 ; :: thesis: contradiction
then u - v,u - v are_Ort_wrt w,y by A1, Th32;
then u - v = 0. V by A1, ANALMETR:11;
hence contradiction by A2, RLVECT_1:21; :: thesis: verum