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

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