set O = OwnSymbolsOf S;
set SS = AllSymbolsOf S;
set I = the Interpreter of S,U;
reconsider f = the Interpreter of S,U | (OwnSymbolsOf S) as Function ;
B1: dom f = (OwnSymbolsOf S) /\ (dom the Interpreter of S,U) by RELAT_1:61
.= OwnSymbolsOf S by Lm2, XBOOLE_1:28 ;
take f ; :: thesis: f is S,U -interpreter-like
B2: for s being own Element of S holds
( f . s is Interpreter of s,U & f . s is Function )

proof

let s be own Element of S; :: thesis: ( f . s is Interpreter of s,U & f . s is Function )
s in dom f by B1, FOMODEL1:def 19;
then Z0: f . s = the Interpreter of S,U . s by FUNCT_1:47;
hence f . s is Interpreter of s,U by DefInterpreter2; :: thesis: f . s is Function
thus f . s is Function by Z0, DefInterpreter2; :: thesis: verum

end;

then reconsider ff = f as Interpreter of S,U by DefInterpreter2;

now

let x be set ; :: thesis: ( x in dom f implies ff . x is Function )
assume x in dom f ; :: thesis: ff . x is Function
then reconsider s = x as own Element of S by B1, FOMODEL1:def 19;
ff . s is Function by B2;
hence ff . x is Function ; :: thesis: verum

end;

then ff is Function-yielding by FUNCOP_1:def 6;
hence f is S,U -interpreter-like by DefInterpreterLike; :: thesis: verum