theorem Th9: :: FOMODEL3:9

for U being non empty set
for u1 being Element of U
for S being Language
for l1, l2 being literal Element of S
for psi being wff string of S st not l2 in rng psi holds
for I being Element of U -InterpretersOf S holds ((l1,u1) ReassignIn I) -TruthEval psi = ((l2,u1) ReassignIn I) -TruthEval ((l1,l2) -SymbolSubstIn psi)