for U being non empty set
for S being Language
for l being literal Element of S
for psi being wff string of S
for tt being Element of AllTermsOf S holds
( Depth ((l,tt) SubstIn psi) = Depth psi & ( for I being Element of U -InterpretersOf S holds I -TruthEval ((l,tt) SubstIn psi) = ((l,((I -TermEval) . tt)) ReassignIn I) -TruthEval psi ) )