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

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