theorem :: ORTSP_1:17

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