set II = U -InterpretersOf S;
set IT = (x,u) ReassignIn I;
set O = OwnSymbolsOf S;
set new = {{}} --> u;
set g = x .--> ({{}} --> u);
reconsider xx = x as own Element of S ;
( {x} c= OwnSymbolsOf S & dom (x .--> ({{}} --> u)) = {x} ) by FOMODEL1:def 19, ZFMISC_1:31;
then reconsider G = dom (x .--> ({{}} --> u)) as Subset of (OwnSymbolsOf S) ;
dom ((x,u) ReassignIn I) = (dom I) \/ G by FUNCT_4:def 1
.= (OwnSymbolsOf S) \/ G by PARTFUN1:def 2
.= OwnSymbolsOf S ;
then reconsider ITT = (x,u) ReassignIn I as OwnSymbolsOf S -defined Function by RELAT_1:def 18;
ITT | (OwnSymbolsOf S) = ITT ;
hence (x,u) ReassignIn I is Element of U -InterpretersOf S by Th2; :: thesis: verum