let S be Language; :: thesis: for U being non empty set
for I being Relation st I in U -InterpretersOf S holds
dom I = OwnSymbolsOf S
let U be non empty set ; :: thesis: for I being Relation st I in U -InterpretersOf S holds
dom I = OwnSymbolsOf S
set O = OwnSymbolsOf S;
set II = U -InterpretersOf S;
let I be Relation; :: thesis: ( I in U -InterpretersOf S implies dom I = OwnSymbolsOf S )
assume I in U -InterpretersOf S ; :: thesis: dom I = OwnSymbolsOf S
then consider f being Element of Funcs ((OwnSymbolsOf S),(PFuncs ((U *),(U \/ BOOLEAN)))) such that
A1: ( I = f & f is S,U -interpreter-like ) ;
reconsider ff = f as Function of (OwnSymbolsOf S),(PFuncs ((U *),(U \/ BOOLEAN))) ;
thus dom I = OwnSymbolsOf S by A1, FUNCT_2:def 1; :: thesis: verum