let S be Language; :: thesis: for U being non empty set
for I being S,b₁ -interpreter-like Function
for u1, u2 being Element of U
for m being Nat
for t being b₅ -termal string of S
for n being Nat holds (((I,u1) -TermEval) . (m + 1)) . t = (((I,u2) -TermEval) . ((m + 1) + n)) . t
let U be non empty set ; :: thesis: for I being S,U -interpreter-like Function
for u1, u2 being Element of U
for m being Nat
for t being b₄ -termal string of S
for n being Nat holds (((I,u1) -TermEval) . (m + 1)) . t = (((I,u2) -TermEval) . ((m + 1) + n)) . t
let I be S,U -interpreter-like Function; :: thesis: for u1, u2 being Element of U
for m being Nat
for t being b₃ -termal string of S
for n being Nat holds (((I,u1) -TermEval) . (m + 1)) . t = (((I,u2) -TermEval) . ((m + 1) + n)) . t
let u1, u2 be Element of U; :: thesis: for m being Nat
for t being b₁ -termal string of S
for n being Nat holds (((I,u1) -TermEval) . (m + 1)) . t = (((I,u2) -TermEval) . ((m + 1) + n)) . t
set F = S -firstChar ;
set ST = S -subTerms ;
set A = AllTermsOf S;
set T = S -termsOfMaxDepth ;
set U1 = (I,u1) -TermEval ;
set U2 = (I,u2) -TermEval ;
set SS = AllSymbolsOf S;
defpred S₁[ Nat] means for t being $1 -termal string of S
for n being Nat holds (((I,u1) -TermEval) . ($1 + 1)) . t = (((I,u2) -TermEval) . (($1 + 1) + n)) . t;
A1: S₁[ 0 ]

proof

let t be 0 -termal string of S; :: thesis: for n being Nat holds (((I,u1) -TermEval) . (0 + 1)) . t = (((I,u2) -TermEval) . ((0 + 1) + n)) . t
let n be Nat; :: thesis: (((I,u1) -TermEval) . (0 + 1)) . t = (((I,u2) -TermEval) . ((0 + 1) + n)) . t
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
(((I,u1) -TermEval) . (0 + 1)) . t = (I . ((S -firstChar) . t)) . {} by Lm5
.= (((I,u2) -TermEval) . ((0 + 1) + nn)) . t by Lm5 ;
hence (((I,u1) -TermEval) . (0 + 1)) . t = (((I,u2) -TermEval) . ((0 + 1) + n)) . t ; :: thesis: verum

end;

A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
reconsider K = k + 1 as Element of NAT ;
let t be k + 1 -termal string of S; :: thesis: for n being Nat holds (((I,u1) -TermEval) . ((k + 1) + 1)) . t = (((I,u2) -TermEval) . (((k + 1) + 1) + n)) . t
let n be Nat; :: thesis: (((I,u1) -TermEval) . ((k + 1) + 1)) . t = (((I,u2) -TermEval) . (((k + 1) + 1) + n)) . t
reconsider KK = K + n as Element of NAT by ORDINAL1:def 12;
reconsider tt = t as termal string of S ;
A4: (((I,u1) -TermEval) . K) * (SubTerms t) = (((I,u2) -TermEval) . (K + n)) * (SubTerms t)

proof

set V = SubTerms t;
set l = |.(ar t).|;
reconsider VV = SubTerms t as |.(ar t).| -element FinSequence of AllTermsOf S by FINSEQ_1:def 11;
reconsider kk = k as Element of NAT by ORDINAL1:def 12;
reconsider tx = t as kk + 1 -termal string of S ;
SubTerms tx is (S -termsOfMaxDepth) . kk -valued Function ;
then reconsider VVV = SubTerms t as (S -termsOfMaxDepth) . k -valued Function ;
len VV = |.(ar t).| by CARD_1:def 7;
then A5: dom VVV = Seg |.(ar t).| by FINSEQ_1:def 3;
reconsider U1K = ((I,u1) -TermEval) . K, U2K = ((I,u2) -TermEval) . KK as Function of (AllTermsOf S),U ;
reconsider p = U1K * VV, q = U2K * VV as |.(ar t).| -element FinSequence of U ;
( len p = |.(ar t).| & len q = |.(ar t).| ) by CARD_1:def 7;
then A6: ( dom p = Seg |.(ar t).| & dom q = Seg |.(ar t).| ) by FINSEQ_1:def 3;
for i being object st i in Seg |.(ar t).| holds
p . i = q . i

proof

let i be object ; :: thesis: ( i in Seg |.(ar t).| implies p . i = q . i )
assume A7: i in Seg |.(ar t).| ; :: thesis: p . i = q . i
then reconsider t1 = VVV . i as k -termal string of S by FOMODEL1:def 33, A5, FUNCT_1:102;
p . i = (((I,u1) -TermEval) . K) . t1 by A7, A6, FUNCT_1:12
.= U2K . (VVV . i) by A3
.= q . i by A7, A6, FUNCT_1:12 ;
hence p . i = q . i ; :: thesis: verum

end;

hence (((I,u1) -TermEval) . K) * (SubTerms t) = (((I,u2) -TermEval) . (K + n)) * (SubTerms t) by A6, FUNCT_1:2; :: thesis: verum

end;

(((I,u1) -TermEval) . (K + 1)) . tt = (I . ((S -firstChar) . tt)) . ((((I,u2) -TermEval) . KK) * (SubTerms t)) by Lm5, A4
.= (((I,u2) -TermEval) . (KK + 1)) . tt by Lm5 ;
hence (((I,u1) -TermEval) . ((k + 1) + 1)) . t = (((I,u2) -TermEval) . (((k + 1) + 1) + n)) . t ; :: thesis: verum

end;

for mm being Nat holds S₁[mm] from NAT_1:sch 2(A1, A2);
hence for m being Nat
for t being b₁ -termal string of S
for n being Nat holds (((I,u1) -TermEval) . (m + 1)) . t = (((I,u2) -TermEval) . ((m + 1) + n)) . t ; :: thesis: verum