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

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

end;

let s be own Element of S; :: thesis:
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:

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, FUNCOP_1:def 6, 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 RELAT_1:def 19, A1;
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:

let s be own Element of S; :: thesis:
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:

end;