set I = the S,U -interpreter-like Function;
set O = OwnSymbolsOf S;
set f = the S,U -interpreter-like Function | (OwnSymbolsOf S);
set C = PFuncs ((U *),(U \/ BOOLEAN));
( dom ( the S,U -interpreter-like Function | (OwnSymbolsOf S)) c= OwnSymbolsOf S & rng ( the S,U -interpreter-like Function | (OwnSymbolsOf S)) c= PFuncs ((U *),(U \/ BOOLEAN)) ) ;
then reconsider ff = the S,U -interpreter-like Function | (OwnSymbolsOf S) as Relation of (OwnSymbolsOf S),(PFuncs ((U *),(U \/ BOOLEAN))) by RELSET_1:4;
reconsider fff = ff as Element of Funcs ((OwnSymbolsOf S),(PFuncs ((U *),(U \/ BOOLEAN)))) by FUNCT_2:8;
ex g being Element of Funcs ((OwnSymbolsOf S),(PFuncs ((U *),(U \/ BOOLEAN)))) st
( the S,U -interpreter-like Function | (OwnSymbolsOf S) = g & g is S,U -interpreter-like )

proof

take fff ; :: thesis: ( the S,U -interpreter-like Function | (OwnSymbolsOf S) = fff & fff is S,U -interpreter-like )
thus ( the S,U -interpreter-like Function | (OwnSymbolsOf S) = fff & fff is S,U -interpreter-like ) ; :: thesis: verum

end;

then the S,U -interpreter-like Function | (OwnSymbolsOf S) in U -InterpretersOf S ;
hence for b₁ being set st b₁ = U -InterpretersOf S holds
not b₁ is empty ; :: thesis: verum