:: deftheorem Def22 defines Polish-binOp POLNOT_1:def 28 :
for T being Polish-language
for A being Polish-arity-function of T
for t being Element of T st A . t = 2 holds
for b₄ being BinOp of (Polish-WFF-set (T,A)) holds
( b₄ = Polish-binOp (T,A,t) iff for u, v being FinSequence st u in Polish-WFF-set (T,A) & v in Polish-WFF-set (T,A) holds
b₄ . (u,v) = (Polish-operation (T,A,t)) . (u ^ v) );