let S be Language; for U being non empty set
for I being S,b1 -interpreter-like Function holds I | (OwnSymbolsOf S) in U -InterpretersOf S
let U be non empty set ; for I being S,U -interpreter-like Function holds I | (OwnSymbolsOf S) in U -InterpretersOf S
let I be S,U -interpreter-like Function; I | (OwnSymbolsOf S) in U -InterpretersOf S
set O = OwnSymbolsOf S;
set C = PFuncs ((U *),(U \/ BOOLEAN));
( dom (I | (OwnSymbolsOf S)) c= OwnSymbolsOf S & rng (I | (OwnSymbolsOf S)) c= PFuncs ((U *),(U \/ BOOLEAN)) )
;
then
I | (OwnSymbolsOf S) is Function of (OwnSymbolsOf S),(PFuncs ((U *),(U \/ BOOLEAN)))
by RELSET_1:4;
then
( I | (OwnSymbolsOf S) is S,U -interpreter-like & I | (OwnSymbolsOf S) is Element of Funcs ((OwnSymbolsOf S),(PFuncs ((U *),(U \/ BOOLEAN)))) )
by FUNCT_2:8;
hence
I | (OwnSymbolsOf S) in U -InterpretersOf S
; verum