set T = S -termsOfMaxDepth ;
set A = AllTermsOf S;
let IT1, IT2 be Element of U; :: thesis: ( ( for u1 being Element of U
for mm being Element of NAT st t in (S -termsOfMaxDepth) . mm holds
IT1 = (((I,u1) -TermEval) . (mm + 1)) . t ) & ( for u1 being Element of U
for mm being Element of NAT st t in (S -termsOfMaxDepth) . mm holds
IT2 = (((I,u1) -TermEval) . (mm + 1)) . t ) implies IT1 = IT2 )
assume A2: for u1 being Element of U
for mm being Element of NAT st t in (S -termsOfMaxDepth) . mm holds
IT1 = (((I,u1) -TermEval) . (mm + 1)) . t ; :: thesis: ( ex u1 being Element of U ex mm being Element of NAT st
( t in (S -termsOfMaxDepth) . mm & not IT2 = (((I,u1) -TermEval) . (mm + 1)) . t ) or IT1 = IT2 )
assume A3: for u2 being Element of U
for nn being Element of NAT st t in (S -termsOfMaxDepth) . nn holds
IT2 = (((I,u2) -TermEval) . (nn + 1)) . t ; :: thesis: IT1 = IT2
consider mm being Element of NAT such that
A4: t in (S -termsOfMaxDepth) . mm by FOMODEL1:5;
set u = the Element of U;
IT1 = (((I, the Element of U) -TermEval) . (mm + 1)) . t by A2, A4
.= IT2 by A3, A4 ;
hence IT1 = IT2 ; :: thesis: verum