let S be Language; :: thesis: for U being non empty set

for I being S,b_{1} -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

for I being S,b

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