:: deftheorem Def16r defines Polish-binOp POLNOT_2:def 25 :
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 = 2 holds
for b₅ being BinOp of Q holds
( b₅ = Polish-binOp (T,Q,t) iff for p, q being FinSequence st p in Q & q in Q holds
b₅ . (p,q) = t ^ (p ^ q) );