:: deftheorem Def22 defines Subst4 FOMODEL3:def 22 :
for S being Language
for l being literal Element of S
for t being termal string of S
for f being Element of Funcs ((AllFormulasOf S),(AllFormulasOf S))
for b₅ being sequence of (Funcs ((AllFormulasOf S),(AllFormulasOf S))) holds
( b₅ = (l,t) Subst4 f iff ( b₅ . 0 = f & ( for m being Nat holds b₅ . (m + 1) = (l,t,m,(b₅ . m)) Subst3 ) ) );