:: deftheorem Def3 defines ^^ POLNOT_1:def 3 :
for P being FinSequence-membered set
for b₂ being Function holds
( b₂ = P ^^ iff ( dom b₂ = NAT & b₂ . 0 = {{}} & ( for n being Nat ex Q being FinSequence-membered set st
( Q = b₂ . n & b₂ . (n + 1) = Q ^ P ) ) ) );