:: deftheorem Def46 defines Subst POLNOT_1:def 46 :
for L being non trivial Polish-language
for E being Polish-arity-function of L
for s being Substitution of L,E
for F, b₅ being Polish-WFF of L,E holds
( b₅ = Subst (s,F) iff ex H being Function of (Polish-WFF-set (L,E)),(Polish-WFF-set (L,E)) st
( H is Subst s -recursive & b₅ = H . F ) );