let S be Language; :: thesis: for U being non empty set
for I being S,b₁ -interpreter-like Function holds I | (OwnSymbolsOf S) in U -InterpretersOf S
let U be non empty set ; :: thesis: for I being S,U -interpreter-like Function holds I | (OwnSymbolsOf S) in U -InterpretersOf S
let I be S,U -interpreter-like Function; :: thesis: 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 ; :: thesis: verum