let X be set ; :: thesis: 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 *)
let U be non empty set ; :: thesis: 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 *)
let S1, S2 be Language; :: thesis: 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 *)
set II1 = U -InterpretersOf S1;
set II2 = U -InterpretersOf S2;
let I1 be Element of U -InterpretersOf S1; :: thesis: 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 *)
let I2 be Element of U -InterpretersOf S2; :: thesis: ( I1 | X = I2 | X & the adicity of S1 | X = the adicity of S2 | X implies (I1 -TermEval) | (X *) = (I2 -TermEval) | (X *) )
set E1 = I1 -TermEval ;
set E2 = I2 -TermEval ;
set D = X * ;
set f1 = (I1 -TermEval) | (X *);
set f2 = (I2 -TermEval) | (X *);
set a1 = the adicity of S1;
set a2 = the adicity of S2;
assume ( I1 | X = I2 | X & the adicity of S1 | X = the adicity of S2 | X ) ; :: thesis: (I1 -TermEval) | (X *) = (I2 -TermEval) | (X *)
then ( (I1 -TermEval) | (X *) c= (I2 -TermEval) | (X *) & (I2 -TermEval) | (X *) c= (I1 -TermEval) | (X *) ) by Lm51;
hence (I1 -TermEval) | (X *) = (I2 -TermEval) | (X *) by XBOOLE_0:def 10; :: thesis: verum