theorem Th13: :: ORTSP_1:13

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