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;
now :: thesis: for s1 being own Element of S1 holds I2 . s1 is Interpreter of s1,U
let s1 be own Element of S1; :: thesis: I2 . b1 is Interpreter of b1,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 ;
per cases ( s2 is relational or not s2 is relational ) ;
suppose not s2 is relational ; :: thesis: I2 . b1 is Interpreter of b1,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;
end;
end;
then ( I2 is Interpreter of S1,U & I222 is Function-yielding ) by Def3;
hence I2 is S1,U -interpreter-like ; :: thesis: verum