:: deftheorem defines Polish-operation POLNOT_1:def 26 :
for T being Polish-language
for A being Polish-arity-function of T
for t being Element of T holds Polish-operation (T,A,t) = Polish-operation (T,A,(A . t),t);