for F being Field
for S being OrtSp of F
for a, b, x, y being Element of S st not a _|_ & x = 0. S holds
PProJ (a,b,x,y) = 0. F