set IT = I2 +* I1;
set O1 = OwnSymbolsOf S1;
set O2 = OwnSymbolsOf S2;
set a1 = the adicity of S1;
set a2 = the adicity of S2;
set AS1 = AtomicFormulaSymbolsOf S1;
now :: thesis: for s2 being own Element of S2 holds (I2 +* I1) . s2 is Interpreter of s2,U
let s2 be own Element of S2; :: thesis: (I2 +* I1) . b1 is Interpreter of b1,U
per cases ( s2 in dom I1 or not s2 in dom I1 ) ;
suppose s2 in dom I1 ; :: thesis: (I2 +* I1) . b1 is Interpreter of b1,U
then A1: ( s2 in OwnSymbolsOf S1 & (I2 +* I1) . s2 = I1 . s2 ) by FUNCT_4:13;
then reconsider s1 = s2 as own Element of S1 by FOMODEL1:def 19;
s1 in AtomicFormulaSymbolsOf S1 by FOMODEL1:def 20;
then A2: s1 in dom the adicity of S1 by FUNCT_2:def 1;
reconsider i1 = I1 . s1 as Interpreter of s1,U ;
set m2 = ar s2;
set m1 = ar s1;
the adicity of S2 . s2 = ( the adicity of S2 +* the adicity of S1) . s2 by FOMODEL1:def 41, FUNCT_4:98
.= the adicity of S1 . s2 by FUNCT_4:13, A2 ;
then A3: ar s1 = ar s2 ;
per cases ( s1 is relational or not s1 is relational ) ;
suppose s1 is relational ; :: thesis: (I2 +* I1) . b1 is Interpreter of b1,U
then ( s2 is relational & i1 is Function of (|.(ar s2).| -tuples_on U),BOOLEAN ) by A3, Def2;
hence (I2 +* I1) . s2 is Interpreter of s2,U by A1, Def2; :: thesis: verum
end;
suppose not s1 is relational ; :: thesis: (I2 +* I1) . b1 is Interpreter of b1,U
then ( i1 is Function of (|.(ar s2).| -tuples_on U),U & not s2 is relational ) by A3, Def2;
hence (I2 +* I1) . s2 is Interpreter of s2,U by Def2, A1; :: thesis: verum
end;
end;
end;
suppose not s2 in dom I1 ; :: thesis: (I2 +* I1) . b1 is Interpreter of b1,U
then (I2 +* I1) . s2 = I2 . s2 by FUNCT_4:11;
hence (I2 +* I1) . s2 is Interpreter of s2,U ; :: thesis: verum
end;
end;
end;
then I2 +* I1 is Interpreter of S2,U by Def3;
hence I2 +* I1 is S2,U -interpreter-like ; :: thesis: verum