theorem Th11: :: FOMODEL3:11

for X being set
for U being non empty set
for S1, S2 being Language
for I1 being Element of U -InterpretersOf S1
for I2 being Element of U -InterpretersOf S2 st I1 | X = I2 | X & the adicity of S1 | X = the adicity of S2 | X holds
(I1 -TermEval) | (X *) = (I2 -TermEval) | (X *) by Lm47;