:: deftheorem Def2 defines ProJ ORTSP_1:def 2 :
for F being Field
for S being OrtSp of F
for a, b, x being Element of S st not a _|_ holds
for b₆ being Element of F holds
( b₆ = ProJ (a,b,x) iff for l being Element of F st a _|_ holds
b₆ = l );