theorem Th12: :: ORTSP_1:12

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