:: deftheorem defines Polish-operations POLNOT_1:def 8 :
for P being FinSequence-membered set
for A being Function of P,NAT holds Polish-operations (P,A) = { t where t is Element of P * : ( t in P & A . t <> 0 ) } ;