:: deftheorem defines -closed POLNOT_1:def 15 :
for P being FinSequence-membered set
for A being Function of P,NAT
for Q being FinSequence-membered set holds
( Q is A -closed iff for p being FinSequence
for n being Nat
for q being FinSequence st p in P & n = A . p & q in Q ^^ n holds
p ^ q in Q );