theorem Th18: :: ORTSP_1:18

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