:: deftheorem Def13 defines Polish-operation POLNOT_1:def 12 :
for P being FinSequence-membered set
for A being Function of P,NAT
for n being Nat
for t being FinSequence st t in P holds
for b₅ being Function of ((Polish-expression-set (P,A)) ^^ n),(P *) holds
( b₅ = Polish-operation (P,A,n,t) iff for q being FinSequence st q in dom b₅ holds
b₅ . q = t ^ q );