let m be Nat; :: thesis: for S being Language
for U being non empty set
for u being Element of U
for I being b₁,b₂ -interpreter-like Function holds (((I,u) -TermEval) . (m + 1)) | ((S -termsOfMaxDepth) . m) = (I -TermEval) | ((S -termsOfMaxDepth) . m)
let S be Language; :: thesis: for U being non empty set
for u being Element of U
for I being S,b₁ -interpreter-like Function holds (((I,u) -TermEval) . (m + 1)) | ((S -termsOfMaxDepth) . m) = (I -TermEval) | ((S -termsOfMaxDepth) . 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)) | ((S -termsOfMaxDepth) . m) = (I -TermEval) | ((S -termsOfMaxDepth) . m)
let u be Element of U; :: thesis: for I being S,U -interpreter-like Function holds (((I,u) -TermEval) . (m + 1)) | ((S -termsOfMaxDepth) . m) = (I -TermEval) | ((S -termsOfMaxDepth) . m)
let I be S,U -interpreter-like Function; :: thesis: (((I,u) -TermEval) . (m + 1)) | ((S -termsOfMaxDepth) . m) = (I -TermEval) | ((S -termsOfMaxDepth) . 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 (AllTermsOf S),U ;
reconsider Tm = (S -termsOfMaxDepth) . mm, TM = (S -termsOfMaxDepth) . MM as Subset of (AllTermsOf S) by FOMODEL1:2;
set LH = IM | Tm;
set RH = (I -TermEval) | Tm;
A1: ( dom (IM | Tm) = Tm & dom ((I -TermEval) | Tm) = Tm ) by PARTFUN1:def 2;

now :: thesis: for x being object st x in dom (IM | Tm) holds
(IM | Tm) . x = ((I -TermEval) | Tm) . x

let x be object ; :: thesis: ( x in dom (IM | Tm) implies (IM | Tm) . x = ((I -TermEval) | Tm) . x )
assume A2: x in dom (IM | Tm) ; :: thesis: (IM | Tm) . x = ((I -TermEval) | Tm) . x
then x in Tm null (AllTermsOf S) ;
then reconsider tt = x as Element of AllTermsOf S ;
reconsider ttt = x as Element of Tm by A2;
( ((IM | Tm) . ttt) \+\ (IM . ttt) = {} & (((I -TermEval) | Tm) . ttt) \+\ ((I -TermEval) . ttt) = {} ) ;
then A3: ( (IM | Tm) . x = IM . tt & ((I -TermEval) | Tm) . x = (I -TermEval) . x ) by FOMODEL0:29;
then (IM | Tm) . x = I -TermEval tt by A2, Def8
.= ((I -TermEval) | Tm) . x by A3, Def9 ;
hence (IM | Tm) . x = ((I -TermEval) | Tm) . x ; :: thesis: verum

end;

hence (((I,u) -TermEval) . (m + 1)) | ((S -termsOfMaxDepth) . m) = (I -TermEval) | ((S -termsOfMaxDepth) . m) by A1, FUNCT_1:2; :: thesis: verum