let V be RealLinearSpace; 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; ( 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
; 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; ( u <> v implies PProJ (w,y,(u - v),(u - v)) <> 0 )
assume A2:
u <> v
; PProJ (w,y,(u - v),(u - v)) <> 0
assume
PProJ (w,y,(u - v),(u - v)) = 0
; 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; verum