set T = S -termsOfMaxDepth ;
set A = AllTermsOf S;
consider mm being Element of NAT such that
A1: t in (S -termsOfMaxDepth) . mm by FOMODEL1:5;
set u1 = the Element of U;
reconsider t0 = t as string of S ;
reconsider t1 = t0 as mm -termal string of S by A1, FOMODEL1:def 33;
reconsider mmm = mm + 1 as Element of NAT ;
reconsider f1 = ((I, the Element of U) -TermEval) . mmm as Function of (AllTermsOf S),U ;
reconsider IT = f1 . t as Element of U ;
take IT ; :: thesis: for u1 being Element of U
for mm being Element of NAT st t in (S -termsOfMaxDepth) . mm holds
IT = (((I,u1) -TermEval) . (mm + 1)) . t
let u2 be Element of U; :: thesis: for mm being Element of NAT st t in (S -termsOfMaxDepth) . mm holds
IT = (((I,u2) -TermEval) . (mm + 1)) . t
let nn be Element of NAT ; :: thesis: ( t in (S -termsOfMaxDepth) . nn implies IT = (((I,u2) -TermEval) . (nn + 1)) . t )
assume t in (S -termsOfMaxDepth) . nn ; :: thesis: IT = (((I,u2) -TermEval) . (nn + 1)) . t
then reconsider t2 = t0 as nn -termal string of S by FOMODEL1:def 33;
IT = (((I,u2) -TermEval) . ((mm + 1) + nn)) . t1 by Lm6
.= (((I,u2) -TermEval) . ((nn + 1) + mm)) . t2
.= (((I,u2) -TermEval) . (nn + 1)) . t2 by Lm6 ;
hence IT = (((I,u2) -TermEval) . (nn + 1)) . t ; :: thesis: verum