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 l is X -absent & 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 l is X -absent & 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 l is X -absent & 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 l is X -absent & 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 l is X -absent & 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: ( l is X -absent & 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 A1: ( l is X -absent & X is I -satisfied ) ; :: thesis: X is (l,u) ReassignIn I -satisfied

now :: thesis: for phi being wff string of S st phi in X holds
((l,u) ReassignIn I) -TruthEval phi = 1

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 A2: phi in X ; :: thesis: ((l,u) ReassignIn I) -TruthEval phi = 1
then reconsider Phi = {phi} as Subset of X by ZFMISC_1:31;
A3: I -TruthEval phi = 1 by A1, A2;
l is X /\ Phi -absent by A1;
then not l in no by FOMODEL2:28;
then {l} misses no by ZFMISC_1:50;
then dom (l .--> ({} .--> u)) misses no ;
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 A3, Th13; :: thesis: verum

end;

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