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

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