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 ;
A1: dom f = (OwnSymbolsOf S) /\ (dom the Interpreter of S,U) by RELAT_1:61
.= OwnSymbolsOf S by XBOOLE_1:28, Lm1 ;
take f ; :: thesis: f is S,U -interpreter-like
A2: 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 )
A3: f . s = the Interpreter of S,U . s by FUNCT_1:47, A1, FOMODEL1:def 19;
hence f . s is Interpreter of s,U by Def3; :: thesis: f . s is Function
thus f . s is Function by A3, Def3; :: thesis: verum
end;
then reconsider ff = f as Interpreter of S,U by Def3;
now :: thesis: for x being object st x in dom f holds
ff . x is Function
let x be object ; :: 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 A1, FOMODEL1:def 19;
ff . s is Function by A2;
hence ff . x is Function ; :: thesis: verum
end;
hence f is S,U -interpreter-like by FUNCOP_1:def 6; :: thesis: verum