let S be Language; :: thesis: for U being non empty set
for p being FinSequence
for u being Element of U
for l2 being literal Element of S
for I being S,b₁ -interpreter-like Function st not l2 in rng p holds
(((l2,u) ReassignIn I) -TermEval) . p = (I -TermEval) . p
let U be non empty set ; :: thesis: for p being FinSequence
for u being Element of U
for l2 being literal Element of S
for I being S,U -interpreter-like Function st not l2 in rng p holds
(((l2,u) ReassignIn I) -TermEval) . p = (I -TermEval) . p
let p be FinSequence; :: thesis: for u being Element of U
for l2 being literal Element of S
for I being S,U -interpreter-like Function st not l2 in rng p holds
(((l2,u) ReassignIn I) -TermEval) . p = (I -TermEval) . p
let u be Element of U; :: thesis: for l2 being literal Element of S
for I being S,U -interpreter-like Function st not l2 in rng p holds
(((l2,u) ReassignIn I) -TermEval) . p = (I -TermEval) . p
let l2 be literal Element of S; :: thesis: for I being S,U -interpreter-like Function st not l2 in rng p holds
(((l2,u) ReassignIn I) -TermEval) . p = (I -TermEval) . p
let I be S,U -interpreter-like Function; :: thesis: ( not l2 in rng p implies (((l2,u) ReassignIn I) -TermEval) . p = (I -TermEval) . p )
set tt = p;
set II = U -InterpretersOf S;
set I2 = (l2,u) ReassignIn I;
set f2 = l2 .--> ({} .--> u);
p null {} is {} \/ (rng p) -valued FinSequence ;
then p is FinSequence of rng p by FOMODEL0:26;
then reconsider ttt = p as Element of (rng p) * ;
( (((((l2,u) ReassignIn I) -TermEval) | ((rng p) *)) . ttt) \+\ ((((l2,u) ReassignIn I) -TermEval) . ttt) = {} & (((I -TermEval) | ((rng p) *)) . ttt) \+\ ((I -TermEval) . ttt) = {} ) ;
then A1: ( ((((l2,u) ReassignIn I) -TermEval) | ((rng p) *)) . p = (((l2,u) ReassignIn I) -TermEval) . p & ((I -TermEval) | ((rng p) *)) . p = (I -TermEval) . p ) by FOMODEL0:29;
assume not l2 in rng p ; :: thesis: (((l2,u) ReassignIn I) -TermEval) . p = (I -TermEval) . p
then {l2} misses rng p by ZFMISC_1:50;
then dom (l2 .--> ({} .--> u)) misses rng p ;
then ((l2,u) ReassignIn I) | (rng p) = I | (rng p) by FUNCT_4:72;
hence (((l2,u) ReassignIn I) -TermEval) . p = (I -TermEval) . p by A1, Lm41; :: thesis: verum