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

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

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