set O = OwnSymbolsOf S;
set C = PFuncs ((U *),(U \/ BOOLEAN));
set II = U -InterpretersOf S;
deffunc H₁( Element of OwnSymbolsOf S) -> E -respecting Interpreter of S,U = the E -respecting Interpreter of S,U;
consider f being Function such that
A1: ( dom f = OwnSymbolsOf S & ( for d being Element of OwnSymbolsOf S holds f . d = H₁(d) ) ) from FUNCT_1:sch 4();

now :: thesis: for x being set st x in dom f holds
f . x is Function

let x be set ; :: thesis: ( x in dom f implies f . x is Function )
assume x in dom f ; :: thesis: f . x is Function
then reconsider o = x as Element of OwnSymbolsOf S by A1;
f . o = H₁(o) by A1;
hence f . x is Function ; :: thesis: verum

end;

then A2: f is Function-yielding by FUNCOP_1:def 6;
for s being own Element of S holds f . s is Interpreter of s,U

proof

let s be own Element of S; :: thesis: f . s is Interpreter of s,U
reconsider o = s as Element of OwnSymbolsOf S by FOMODEL1:def 19;
f . o = H₁(o) by A1;
hence f . s is Interpreter of s,U ; :: thesis: verum

end;

then reconsider ff = f as Interpreter of S,U by FOMODEL2:def 3;
reconsider fff = ff as S,U -interpreter-like Function by A2, FOMODEL2:def 4;
reconsider ffff = fff as OwnSymbolsOf S -defined Function by A1, RELAT_1:def 18;
( fff | (OwnSymbolsOf S) is PFuncs ((U *),(U \/ BOOLEAN)) -valued & ffff | (OwnSymbolsOf S) = ffff null (OwnSymbolsOf S) ) ;
then ( fff = fff & dom fff = OwnSymbolsOf S & rng fff c= PFuncs ((U *),(U \/ BOOLEAN)) ) by A1, RELAT_1:def 19;
then reconsider IT = fff as Element of Funcs ((OwnSymbolsOf S),(PFuncs ((U *),(U \/ BOOLEAN)))) by FUNCT_2:def 2;
IT in U -InterpretersOf S ;
then reconsider ITT = IT as Element of U -InterpretersOf S ;
take ITT ; :: thesis: ITT is E -respecting

now :: thesis: for s being own Element of S holds ITT . s is E -respecting

let s be own Element of S; :: thesis: ITT . s is E -respecting
reconsider o = s as Element of OwnSymbolsOf S by FOMODEL1:def 19;
fff . o = H₁(o) by A1;
hence ITT . s is E -respecting ; :: thesis: verum

end;

hence ITT is E -respecting by Def16; :: thesis: verum