theorem Th39: :: POLNOT_1:39

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