let m be Nat; :: thesis: for S being Language
for U being non empty set
for u being Element of U
for I being b1,b2 -interpreter-like Function holds (((I,u) -TermEval) . (m + 1)) | (() . m) = () | (() . m)

let S be Language; :: thesis: for U being non empty set
for u being Element of U
for I being S,b1 -interpreter-like Function holds (((I,u) -TermEval) . (m + 1)) | (() . m) = () | (() . m)

let U be non empty set ; :: thesis: for u being Element of U
for I being S,U -interpreter-like Function holds (((I,u) -TermEval) . (m + 1)) | (() . m) = () | (() . m)

let u be Element of U; :: thesis: for I being S,U -interpreter-like Function holds (((I,u) -TermEval) . (m + 1)) | (() . m) = () | (() . m)
let I be S,U -interpreter-like Function; :: thesis: (((I,u) -TermEval) . (m + 1)) | (() . m) = () | (() . m)
reconsider mm = m, MM = m + 1 as Element of NAT by ORDINAL1:def 12;
set T = S -termsOfMaxDepth ;
set TI = I -TermEval ;
set TII = (I,u) -TermEval ;
set TT = AllTermsOf S;
reconsider IM = ((I,u) -TermEval) . MM as Function of (),U ;
reconsider Tm = () . mm, TM = () . MM as Subset of () by FOMODEL1:2;
set LH = IM | Tm;
set RH = () | Tm;
A1: ( dom (IM | Tm) = Tm & dom (() | Tm) = Tm ) by PARTFUN1:def 2;
now :: thesis: for x being object st x in dom (IM | Tm) holds
(IM | Tm) . x = (() | Tm) . x
let x be object ; :: thesis: ( x in dom (IM | Tm) implies (IM | Tm) . x = (() | Tm) . x )
assume A2: x in dom (IM | Tm) ; :: thesis: (IM | Tm) . x = (() | Tm) . x
then x in Tm null () ;
then reconsider tt = x as Element of AllTermsOf S ;
reconsider ttt = x as Element of Tm by A2;
( ((IM | Tm) . ttt) \+\ (IM . ttt) = {} & ((() | Tm) . ttt) \+\ (() . ttt) = {} ) ;
then A3: ( (IM | Tm) . x = IM . tt & (() | Tm) . x = () . x ) by FOMODEL0:29;
then (IM | Tm) . x = I -TermEval tt by
.= (() | Tm) . x by ;
hence (IM | Tm) . x = (() | Tm) . x ; :: thesis: verum
end;
hence (((I,u) -TermEval) . (m + 1)) | (() . m) = () | (() . m) by ; :: thesis: verum