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;

hence I2 +* I1 is S2,U -interpreter-like ; :: thesis: verum

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

then
I2 +* I1 is Interpreter of S2,U
by Def3;let s2 be own Element of S2; :: thesis: (I2 +* I1) . b_{1} is Interpreter of b_{1},U

end;per cases
( s2 in dom I1 or not s2 in dom I1 )
;

end;

suppose
s2 in dom I1
; :: thesis: (I2 +* I1) . b_{1} is Interpreter of b_{1},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 ;

end;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 )
;

end;

suppose
s1 is relational
; :: thesis: (I2 +* I1) . b_{1} is Interpreter of b_{1},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;hence (I2 +* I1) . s2 is Interpreter of s2,U by A1, Def2; :: thesis: verum

suppose
not s1 is relational
; :: thesis: (I2 +* I1) . b_{1} is Interpreter of b_{1},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;hence (I2 +* I1) . s2 is Interpreter of s2,U by Def2, A1; :: thesis: verum

suppose
not s2 in dom I1
; :: thesis: (I2 +* I1) . b_{1} is Interpreter of b_{1},U

then
(I2 +* I1) . s2 = I2 . s2
by FUNCT_4:11;

hence (I2 +* I1) . s2 is Interpreter of s2,U ; :: thesis: verum

end;hence (I2 +* I1) . s2 is Interpreter of s2,U ; :: thesis: verum

hence I2 +* I1 is S2,U -interpreter-like ; :: thesis: verum