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