for P being FinSequence-membered set
for A being Function of P,NAT
for r being FinSequence st r in Polish-expression-set (P,A) holds
ex n being Nat ex t, q being FinSequence st
( t in P & n = A . t & r = (Polish-operation (P,A,n,t)) . q )