:: deftheorem Def15 defines Polish-unOp POLNOT_2:def 11 :
for B being Polish-arity-function
for Z being b₁ -closed Polish-language
for p being FinSequence st p in dom B & B . p = 1 holds
for b₄ being UnOp of Z holds
( b₄ = Polish-unOp (B,Z,p) iff for q being FinSequence st q in Z holds
b₄ . q = p ^ q );