:: deftheorem Def15r defines Polish-unOp POLNOT_2:def 24 :
for T being Polish-language
for V being full Polish-language of T
for Q being Extension of V
for t being Element of T st (Polish-arity V) . t = 1 holds
for b₅ being UnOp of Q holds
( b₅ = Polish-unOp (T,Q,t) iff for p being FinSequence st p in Q holds
b₅ . p = t ^ p );