:: deftheorem Def20 defines Subst2 FOMODEL3:def 20 :
for S being Language
for l being literal Element of S
for t being termal string of S
for n being Nat
for f being FinSequence-yielding Function
for phi being wff string of S holds
( ( Depth phi = n + 1 & not phi is exal implies (l,t,n,f) Subst2 phi = (<*(TheNorSymbOf S)*> ^ (f . (head phi))) ^ (f . (tail phi)) ) & ( Depth phi = n + 1 & phi is exal & (S -firstChar) . phi <> l implies (l,t,n,f) Subst2 phi = <* the Element of (LettersOf S) \ (((rng t) \/ (rng (head phi))) \/ {l})*> ^ (f . ((((S -firstChar) . phi), the Element of (LettersOf S) \ (((rng t) \/ (rng (head phi))) \/ {l})) -SymbolSubstIn (head phi))) ) & ( ( not Depth phi = n + 1 or phi is exal ) & ( not Depth phi = n + 1 or not phi is exal or not (S -firstChar) . phi <> l ) implies (l,t,n,f) Subst2 phi = f . phi ) );