let S be Language; 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,b1 -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 ; 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; 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; 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; 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; ( 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
; (((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; verum