theorem Th32: :: POLNOT_1:32

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 p, q being FinSequence st
( p in P & n = A . p & q in (Polish-expression-set (P,A)) ^^ n & r = p ^ q )