set O1 = OwnSymbolsOf S1;

set O2 = OwnSymbolsOf S2;

set a1 = the adicity of S1;

set a2 = the adicity of S2;

set AS1 = AtomicFormulaSymbolsOf S1;

set E2 = TheEqSymbOf S2;

set AS2 = AtomicFormulaSymbolsOf S2;

set E1 = TheEqSymbOf S1;

let I2 be Function; :: thesis: ( I2 is S2,U -interpreter-like implies I2 is S1,U -interpreter-like )

assume I2 is S2,U -interpreter-like ; :: thesis: I2 is S1,U -interpreter-like

then reconsider I222 = I2 as S2,U -interpreter-like Function ;

reconsider I22 = I222 as Interpreter of S2,U by Def4;

(OwnSymbolsOf S1) \ (OwnSymbolsOf S2) = {} ;

then A1: ( OwnSymbolsOf S1 c= OwnSymbolsOf S2 & dom the adicity of S1 = AtomicFormulaSymbolsOf S1 & dom the adicity of S2 = AtomicFormulaSymbolsOf S2 ) by XBOOLE_1:37, FUNCT_2:def 1;

the adicity of S1 c= the adicity of S2 by FOMODEL1:def 41;

then A2: dom the adicity of S1 c= dom the adicity of S2 by RELAT_1:11;

hence I2 is S1,U -interpreter-like ; :: thesis: verum

set O2 = OwnSymbolsOf S2;

set a1 = the adicity of S1;

set a2 = the adicity of S2;

set AS1 = AtomicFormulaSymbolsOf S1;

set E2 = TheEqSymbOf S2;

set AS2 = AtomicFormulaSymbolsOf S2;

set E1 = TheEqSymbOf S1;

let I2 be Function; :: thesis: ( I2 is S2,U -interpreter-like implies I2 is S1,U -interpreter-like )

assume I2 is S2,U -interpreter-like ; :: thesis: I2 is S1,U -interpreter-like

then reconsider I222 = I2 as S2,U -interpreter-like Function ;

reconsider I22 = I222 as Interpreter of S2,U by Def4;

(OwnSymbolsOf S1) \ (OwnSymbolsOf S2) = {} ;

then A1: ( OwnSymbolsOf S1 c= OwnSymbolsOf S2 & dom the adicity of S1 = AtomicFormulaSymbolsOf S1 & dom the adicity of S2 = AtomicFormulaSymbolsOf S2 ) by XBOOLE_1:37, FUNCT_2:def 1;

the adicity of S1 c= the adicity of S2 by FOMODEL1:def 41;

then A2: dom the adicity of S1 c= dom the adicity of S2 by RELAT_1:11;

now :: thesis: for s1 being own Element of S1 holds I2 . s1 is Interpreter of s1,U

then
( I2 is Interpreter of S1,U & I222 is Function-yielding )
by Def3;let s1 be own Element of S1; :: thesis: I2 . b_{1} is Interpreter of b_{1},U

A3: s1 in AtomicFormulaSymbolsOf S1 by FOMODEL1:def 20;

then A4: s1 in dom the adicity of S1 by FUNCT_2:def 1;

s1 in AtomicFormulaSymbolsOf S2 by A3, A2, A1;

then reconsider s2 = s1 as ofAtomicFormula Element of S2 by FOMODEL1:def 20;

s1 <> TheEqSymbOf S1 ;

then ( s2 <> TheEqSymbOf S2 & s2 <> TheNorSymbOf S2 ) by FOMODEL1:def 41;

then s2 is Element of OwnSymbolsOf S2 by FOMODEL1:15;

then reconsider s2 = s2 as own Element of S2 by FOMODEL1:def 19;

reconsider i2 = I22 . s2 as Interpreter of s2,U by Def3;

set m2 = ar s2;

set m1 = ar s1;

the adicity of S2 . s2 = ( the adicity of S2 +* the adicity of S1) . s2 by FUNCT_4:98, FOMODEL1:def 41

.= the adicity of S1 . s2 by FUNCT_4:13, A4 ;

then A5: ar s1 = ar s2 ;

end;A3: s1 in AtomicFormulaSymbolsOf S1 by FOMODEL1:def 20;

then A4: s1 in dom the adicity of S1 by FUNCT_2:def 1;

s1 in AtomicFormulaSymbolsOf S2 by A3, A2, A1;

then reconsider s2 = s1 as ofAtomicFormula Element of S2 by FOMODEL1:def 20;

s1 <> TheEqSymbOf S1 ;

then ( s2 <> TheEqSymbOf S2 & s2 <> TheNorSymbOf S2 ) by FOMODEL1:def 41;

then s2 is Element of OwnSymbolsOf S2 by FOMODEL1:15;

then reconsider s2 = s2 as own Element of S2 by FOMODEL1:def 19;

reconsider i2 = I22 . s2 as Interpreter of s2,U by Def3;

set m2 = ar s2;

set m1 = ar s1;

the adicity of S2 . s2 = ( the adicity of S2 +* the adicity of S1) . s2 by FUNCT_4:98, FOMODEL1:def 41

.= the adicity of S1 . s2 by FUNCT_4:13, A4 ;

then A5: ar s1 = ar s2 ;

per cases
( s2 is relational or not s2 is relational )
;

end;

suppose
s2 is relational
; :: thesis: I2 . b_{1} is Interpreter of b_{1},U

then
( s1 is relational & i2 is Function of (|.(ar s1).| -tuples_on U),BOOLEAN )
by A5, Def2;

hence I2 . s1 is Interpreter of s1,U by Def2; :: thesis: verum

end;hence I2 . s1 is Interpreter of s1,U by Def2; :: thesis: verum

suppose
not s2 is relational
; :: thesis: I2 . b_{1} is Interpreter of b_{1},U

then
( i2 is Function of (|.(ar s1).| -tuples_on U),U & not s1 is relational )
by A5, Def2;

hence I2 . s1 is Interpreter of s1,U by Def2; :: thesis: verum

end;hence I2 . s1 is Interpreter of s1,U by Def2; :: thesis: verum

hence I2 is S1,U -interpreter-like ; :: thesis: verum