let X be set ; :: thesis: for U being non empty set
for u being Element of U
for S being Language
for l being literal Element of S
for I being Element of U -InterpretersOf S st not l is X -occurring & X is I -satisfied holds
X is (l,u) ReassignIn I -satisfied
let U be non empty set ; :: thesis: for u being Element of U
for S being Language
for l being literal Element of S
for I being Element of U -InterpretersOf S st not l is X -occurring & X is I -satisfied holds
X is (l,u) ReassignIn I -satisfied
let u be Element of U; :: thesis: for S being Language
for l being literal Element of S
for I being Element of U -InterpretersOf S st not l is X -occurring & X is I -satisfied holds
X is (l,u) ReassignIn I -satisfied
let S be Language; :: thesis: for l being literal Element of S
for I being Element of U -InterpretersOf S st not l is X -occurring & X is I -satisfied holds
X is (l,u) ReassignIn I -satisfied
let l be literal Element of S; :: thesis: for I being Element of U -InterpretersOf S st not l is X -occurring & X is I -satisfied holds
X is (l,u) ReassignIn I -satisfied
set II = U -InterpretersOf S;
let I be Element of U -InterpretersOf S; :: thesis: ( not l is X -occurring & X is I -satisfied implies X is (l,u) ReassignIn I -satisfied )
set O = OwnSymbolsOf S;
set I2 = (l,u) ReassignIn I;
set f2 = l .--> ({} .--> u);
assume B0: ( not l is X -occurring & X is I -satisfied ) ; :: thesis: X is (l,u) ReassignIn I -satisfied

now

let phi be wff string of S; :: thesis: ( phi in X implies ((l,u) ReassignIn I) -TruthEval phi = 1 )
reconsider no = (rng phi) /\ (OwnSymbolsOf S) as Subset of (rng phi) ;
assume C0: phi in X ; :: thesis: ((l,u) ReassignIn I) -TruthEval phi = 1
then reconsider Phi = {phi} as Subset of X by ZFMISC_1:31;
C1: I -TruthEval phi = 1 by B0, C0, FOMODEL2:def 42;
not l is X /\ Phi -occurring by B0;
then not l in no by FOMODEL2:28;
then {l} misses no by ZFMISC_1:50;
then dom (l .--> ({} .--> u)) misses no by FUNCOP_1:13;
then (I | no) +* ((l .--> ({} .--> u)) | no) = (I | no) null {} by RELAT_1:66;
then ((l,u) ReassignIn I) | no = I | no by FUNCT_4:71;
hence ((l,u) ReassignIn I) -TruthEval phi = 1 by C1, Th13; :: thesis: verum

end;

hence X is (l,u) ReassignIn I -satisfied by FOMODEL2:def 42; :: thesis: verum