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_{1},b_{2} -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_{1} -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;

for U being non empty set

for u being Element of U

for I being b

let S be Language; :: thesis: for U being non empty set

for u being Element of U

for I being S,b

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

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