:: deftheorem Def45 defines Subst POLNOT_1:def 45 :
for L being non trivial Polish-language
for E being Polish-arity-function of L
for s being Substitution of L,E
for b₄ being Polish-recursion-function of E,(Polish-WFF-set (L,E)) holds
( b₄ = Subst s iff for t being Element of L
for p being FinSequence of Polish-WFF-set (L,E) st len p = E . t holds
( ( t in dom s implies b₄ . (t,p) = s . t ) & ( not t in dom s implies b₄ . (t,p) = t ^ (FlattenSeq p) ) ) );