:: deftheorem Def3 defines PProJ ORTSP_1:def 3 :
for F being Field
for S being OrtSp of F
for x, y, a, b being Element of S st not a _|_ holds
for b₇ being Element of F holds
( ( ex p being Element of S st
( not a _|_ & not x _|_ ) implies ( b₇ = PProJ (a,b,x,y) iff for q being Element of S st not a _|_ & not x _|_ holds
b₇ = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) ) ) & ( ( for p being Element of S holds
( a _|_ or x _|_ ) ) implies ( b₇ = PProJ (a,b,x,y) iff b₇ = 0. F ) ) );