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 )

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

then reconsider ff = f as Interpreter of S,U by Def3;
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;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

now :: thesis: for x being object st x in dom f holds

ff . x is Function

hence
f is S,U -interpreter-like
by FUNCOP_1:def 6; :: thesis: verumff . 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;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