:: deftheorem Def21 defines Subst3 FOMODEL3:def 21 :
for S being Language
for l being literal Element of S
for t being termal string of S
for n being Nat
for f, b₆ being Element of Funcs ((AllFormulasOf S),(AllFormulasOf S)) holds
( b₆ = (l,t,n,f) Subst3 iff for phi being wff string of S holds b₆ . phi = (l,t,n,f) Subst2 phi );