set O = OwnSymbolsOf S;
set II = U -InterpretersOf S;
let I be OwnSymbolsOf S -defined Element of U -InterpretersOf S; :: thesis: I is total
dom I = OwnSymbolsOf S by Lm32;
hence I is total by PARTFUN1:def 2; :: thesis: verum