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 DefInterpreterLike;
(OwnSymbolsOf S1) \ (OwnSymbolsOf S2) = {} ;
then B0: ( OwnSymbolsOf S1 c= OwnSymbolsOf S2 & dom the adicity of S1 = AtomicFormulaSymbolsOf S1 & dom the adicity of S2 = AtomicFormulaSymbolsOf S2 ) by FUNCT_2:def 1, XBOOLE_1:37;
the adicity of S1 c= the adicity of S2 by FOMODEL1:def 41;
then B1: dom the adicity of S1 c= dom the adicity of S2 by RELAT_1:11;

now

let s1 be own Element of S1; :: thesis: I2 . b₁ is Interpreter of b₁,U
Z0: s1 in AtomicFormulaSymbolsOf S1 by FOMODEL1:def 20;
then C2: s1 in dom the adicity of S1 by FUNCT_2:def 1;
s1 in AtomicFormulaSymbolsOf S2 by Z0, B1, B0;
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 DefInterpreter2;
set m2 = ar s2;
set m1 = ar s1;
the adicity of S1 c= the adicity of S2 by FOMODEL1:def 41;
then the adicity of S2 . s2 = ( the adicity of S2 +* the adicity of S1) . s2 by FUNCT_4:98
.= the adicity of S1 . s2 by C2, FUNCT_4:13 ;
then C0: ar s1 = ar s2 ;

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

suppose s2 is relational ; :: thesis: I2 . b₁ is Interpreter of b₁,U

then ( s1 is relational & i2 is Function of ((abs (ar s1)) -tuples_on U),BOOLEAN ) by C0, DefInterpreter1;
hence I2 . s1 is Interpreter of s1,U by DefInterpreter1; :: thesis: verum

end;

suppose not s2 is relational ; :: thesis: I2 . b₁ is Interpreter of b₁,U

then ( i2 is Function of ((abs (ar s1)) -tuples_on U),U & not s1 is relational ) by C0, DefInterpreter1;
hence I2 . s1 is Interpreter of s1,U by DefInterpreter1; :: thesis: verum

end;

end;

end;

then ( I2 is Interpreter of S1,U & I222 is Function-yielding ) by DefInterpreter2;
hence I2 is S1,U -interpreter-like by DefInterpreterLike; :: thesis: verum