theorem :: ORTSP_1:16

for F being Field
for S being OrtSp of F
for a, b, c, p being Element of S st not a _|_ & a _|_ holds
( ProJ (a,(b + p),c) = ProJ (a,b,c) & ProJ (a,b,(c + p)) = ProJ (a,b,c) )