let S be Language; :: thesis: for U being non empty set
for I being S,b1 -interpreter-like Function
for u1, u2 being Element of U
for m being Nat
for t being b5 -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 b4 -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 b3 -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 b1 -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 S1[ 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: S1[ 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 . (() . 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 S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; :: thesis: S1[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) * () = (((I,u2) -TermEval) . (K + n)) * ()
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 () . kk -valued Function ;
then reconsider VVV = SubTerms t as () . 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 (),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 ;
p . i = (((I,u1) -TermEval) . K) . t1 by
.= U2K . (VVV . i) by A3
.= q . i by ;
hence p . i = q . i ; :: thesis: verum
end;
hence (((I,u1) -TermEval) . K) * () = (((I,u2) -TermEval) . (K + n)) * () by ; :: thesis: verum
end;
(((I,u1) -TermEval) . (K + 1)) . tt = (I . (() . tt)) . ((((I,u2) -TermEval) . KK) * ()) by
.= (((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 S1[mm] from NAT_1:sch 2(A1, A2);
hence for m being Nat
for t being b1 -termal string of S
for n being Nat holds (((I,u1) -TermEval) . (m + 1)) . t = (((I,u2) -TermEval) . ((m + 1) + n)) . t ; :: thesis: verum