let U be non empty set ; :: thesis: for u being Element of U
for m being Nat
for S being Language
for l1, l2 being literal Element of S
for I being b₃,U -interpreter-like Function holds (((l1,u) ReassignIn I) -TermEval) | ((((AllSymbolsOf S) \ {l2}) *) /\ ((S -termsOfMaxDepth) . m)) = ((((l2,u) ReassignIn I) -TermEval) * (l1 SubstWith l2)) | ((((AllSymbolsOf S) \ {l2}) *) /\ ((S -termsOfMaxDepth) . m))
let u be Element of U; :: thesis: for m being Nat
for S being Language
for l1, l2 being literal Element of S
for I being b₂,U -interpreter-like Function holds (((l1,u) ReassignIn I) -TermEval) | ((((AllSymbolsOf S) \ {l2}) *) /\ ((S -termsOfMaxDepth) . m)) = ((((l2,u) ReassignIn I) -TermEval) * (l1 SubstWith l2)) | ((((AllSymbolsOf S) \ {l2}) *) /\ ((S -termsOfMaxDepth) . m))
let m be Nat; :: thesis: for S being Language
for l1, l2 being literal Element of S
for I being b₁,U -interpreter-like Function holds (((l1,u) ReassignIn I) -TermEval) | ((((AllSymbolsOf S) \ {l2}) *) /\ ((S -termsOfMaxDepth) . m)) = ((((l2,u) ReassignIn I) -TermEval) * (l1 SubstWith l2)) | ((((AllSymbolsOf S) \ {l2}) *) /\ ((S -termsOfMaxDepth) . m))
let S be Language; :: thesis: for l1, l2 being literal Element of S
for I being S,U -interpreter-like Function holds (((l1,u) ReassignIn I) -TermEval) | ((((AllSymbolsOf S) \ {l2}) *) /\ ((S -termsOfMaxDepth) . m)) = ((((l2,u) ReassignIn I) -TermEval) * (l1 SubstWith l2)) | ((((AllSymbolsOf S) \ {l2}) *) /\ ((S -termsOfMaxDepth) . m))
let l1, l2 be literal Element of S; :: thesis: for I being S,U -interpreter-like Function holds (((l1,u) ReassignIn I) -TermEval) | ((((AllSymbolsOf S) \ {l2}) *) /\ ((S -termsOfMaxDepth) . m)) = ((((l2,u) ReassignIn I) -TermEval) * (l1 SubstWith l2)) | ((((AllSymbolsOf S) \ {l2}) *) /\ ((S -termsOfMaxDepth) . m))
let I be S,U -interpreter-like Function; :: thesis: (((l1,u) ReassignIn I) -TermEval) | ((((AllSymbolsOf S) \ {l2}) *) /\ ((S -termsOfMaxDepth) . m)) = ((((l2,u) ReassignIn I) -TermEval) * (l1 SubstWith l2)) | ((((AllSymbolsOf S) \ {l2}) *) /\ ((S -termsOfMaxDepth) . m))
set I1 = (l1,u) ReassignIn I;
set I2 = (l2,u) ReassignIn I;
set s = l1 SubstWith l2;
set E1 = ((l1,u) ReassignIn I) -TermEval ;
set E2 = ((l2,u) ReassignIn I) -TermEval ;
set T = S -termsOfMaxDepth ;
set TT = AllTermsOf S;
set SS = AllSymbolsOf S;
set F = S -firstChar ;
set C = S -multiCat ;
set g1 = l1 .--> ({} .--> u);
set g2 = l2 .--> ({} .--> u);
set L = LettersOf S;
reconsider SSS = (AllSymbolsOf S) \ {l2} as non empty Subset of (AllSymbolsOf S) ;
set D = SSS * ;
( l1 in {l1} & l2 in {l2} ) by TARSKI:def 1;
then ( l1 in dom (l1 .--> ({} .--> u)) & l2 in dom (l2 .--> ({} .--> u)) ) ;
then ( ((l1,u) ReassignIn I) . l1 = (l1 .--> ({} .--> u)) . l1 & ((l2,u) ReassignIn I) . l2 = (l2 .--> ({} .--> u)) . l2 ) by FUNCT_4:13;
then A1: ( ((l1,u) ReassignIn I) . l1 = {} .--> u & ((l2,u) ReassignIn I) . l2 = {} .--> u ) by FUNCOP_1:72;
defpred S₁[ Nat] means (((l1,u) ReassignIn I) -TermEval) | (((S -termsOfMaxDepth) . $1) /\ (SSS *)) = ((((l2,u) ReassignIn I) -TermEval) * (l1 SubstWith l2)) | (((S -termsOfMaxDepth) . $1) /\ (SSS *));
A2: S₁[ 0 ]

proof

reconsider T0 = (S -termsOfMaxDepth) . 0 as non empty Subset of (AllTermsOf S) by FOMODEL1:2;
reconsider T00 = T0 as non empty Subset of ((AllSymbolsOf S) *) by XBOOLE_1:1;
reconsider ss = (l1 SubstWith l2) | ((S -termsOfMaxDepth) . 0) as (S -termsOfMaxDepth) . 0 -valued Function ;
reconsider X0 = T0 /\ (SSS *) as Subset of T0 ;
reconsider X = T0 /\ (SSS *) as Subset of (AllTermsOf S) by XBOOLE_1:1;
ss | (SSS *) is T0 -valued ;
then reconsider sss = (l1 SubstWith l2) | (T0 /\ (SSS *)) as T00 -valued Function by RELAT_1:71;
A3: ( dom ((((l2,u) ReassignIn I) -TermEval) * sss) = X & dom ((((l1,u) ReassignIn I) -TermEval) | X) = X ) by PARTFUN1:def 2;
( rng ((((l2,u) ReassignIn I) -TermEval) * sss) c= U & rng ((((l1,u) ReassignIn I) -TermEval) | X) c= U ) by RELAT_1:def 19;
then reconsider f1 = (((l1,u) ReassignIn I) -TermEval) | X, f2 = (((l2,u) ReassignIn I) -TermEval) * sss as Function of X,U by FUNCT_2:2, A3;

now :: thesis: for x being object st x in X holds
f1 . x = f2 . x

let x be object ; :: thesis: ( x in X implies f1 . b₁ = f2 . b₁ )
assume A4: x in X ; :: thesis: f1 . b₁ = f2 . b₁
then reconsider X00 = X0 as non empty Subset of (SSS *) ;
( dom sss = X & rng sss c= T0 ) by PARTFUN1:def 2, RELAT_1:def 19;
then reconsider ssss = sss as Function of X00,T0 by FUNCT_2:2;
reconsider xx = x as Element of X00 by A4;
reconsider xd = xx as Element of SSS * ;
reconsider t0 = x as 0 -termal string of S by TARSKI:def 3, FOMODEL1:def 33, A4;
reconsider t00 = t0 as Element of T0 by FOMODEL1:def 33;
T0 = AtomicTermsOf S by FOMODEL1:def 30;
then reconsider tl = t00 as 1 -element FinSequence of LettersOf S by FOMODEL0:12;
reconsider LL = (LettersOf S) \ {l2} as non empty Subset of (LettersOf S) ;
( rng tl c= LettersOf S & rng xd c= (AllSymbolsOf S) \ {l2} ) by RELAT_1:def 19;
then rng xx c= (LettersOf S) /\ ((AllSymbolsOf S) \ {l2}) by XBOOLE_1:19;
then rng xx c= ((LettersOf S) null (AllSymbolsOf S)) \ {l2} by XBOOLE_1:49;
then reconsider xxx = tl as LL -valued 1 -element FinSequence by RELAT_1:def 19;
{(xxx . 1)} \ LL = {} ;
then reconsider lx = xxx . 1 as Element of LL by ZFMISC_1:60;
not lx in {l2} by XBOOLE_0:def 5;
then A5: ( lx <> l2 & not lx in dom (l2 .--> ({} .--> u)) ) by TARSKI:def 1;
A6: len xxx = 1 by CARD_1:def 7;
reconsider newt = (l1,l2) -SymbolSubstIn t0 as 0 -termal string of S ;
reconsider s1 = (S -firstChar) . t0, s2 = (S -firstChar) . newt as literal Element of S ;
A7: ( s1 = lx & s2 = newt . 1 ) by FOMODEL0:6;
( (((((l2,u) ReassignIn I) -TermEval) * ssss) . xx) \+\ ((((l2,u) ReassignIn I) -TermEval) . (ssss . xx)) = {} & (sss . xx) \+\ ((l1 SubstWith l2) . xx) = {} & (f1 . xx) \+\ ((((l1,u) ReassignIn I) -TermEval) . xx) = {} ) ;
then A8: ( ((((l2,u) ReassignIn I) -TermEval) * sss) . x = (((l2,u) ReassignIn I) -TermEval) . (sss . x) & sss . x = (l1 SubstWith l2) . x & f1 . x = (((l1,u) ReassignIn I) -TermEval) . x ) by FOMODEL0:29;
A9: f2 . x = (((l2,u) ReassignIn I) -TermEval) . newt by A8, FOMODEL0:def 22
.= (((l2,u) ReassignIn I) . s2) . ((((l2,u) ReassignIn I) -TermEval) * (SubTerms newt)) by FOMODEL2:21
.= (((l2,u) ReassignIn I) . s2) . {} ;
A10: f1 . x = (((l1,u) ReassignIn I) . s1) . ((((l1,u) ReassignIn I) -TermEval) * (SubTerms t0)) by A8, FOMODEL2:21
.= (((l1,u) ReassignIn I) . s1) . {} ;

per cases ( lx = l1 or lx <> l1 ) ;

suppose A11: lx = l1 ; :: thesis: f1 . b₁ = f2 . b₁

t0 = <*l1*> by A6, FINSEQ_1:40, A11;
then newt = <*l2*> by FOMODEL0:34;
hence f1 . x = f2 . x by A11, A10, A1, A9, A7; :: thesis: verum

end;

suppose lx <> l1 ; :: thesis: f1 . b₁ = f2 . b₁

then ( newt . 1 = lx & not lx in {l1} ) by FUNCT_4:105, TARSKI:def 1;
then ( s2 = lx & not lx in dom (l1 .--> ({} .--> u)) ) by FOMODEL0:6;
then ( f2 . x = (I . lx) . {} & f1 . x = (I . lx) . {} ) by A7, A9, A10, FUNCT_4:11, A5;
hence f1 . x = f2 . x ; :: thesis: verum

end;

end;

end;

then f1 = f2 by FUNCT_2:12;
hence S₁[ 0 ] by RELAT_1:83; :: thesis: verum

end;

A12: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
reconsider nn = n, NN = n + 1 as Element of NAT by ORDINAL1:def 12;
assume A13: S₁[n] ; :: thesis: S₁[n + 1]
reconsider Tnn = (S -termsOfMaxDepth) . nn, TNN = (S -termsOfMaxDepth) . NN as non empty Subset of (AllTermsOf S) by FOMODEL1:2;
reconsider Xn = Tnn /\ (SSS *), X = TNN /\ (SSS *) as Subset of (AllTermsOf S) by XBOOLE_1:1;
((l1 SubstWith l2) | ((S -termsOfMaxDepth) . NN)) | (SSS *) is TNN -valued ;
then reconsider sX = (l1 SubstWith l2) | X as AllTermsOf S -valued Function by RELAT_1:71;
( dom ((l1 SubstWith l2) | X) = X & rng sX c= AllTermsOf S ) by PARTFUN1:def 2, RELAT_1:def 19;
then reconsider sXX = sX as Function of X,(AllTermsOf S) by FUNCT_2:2;
((l1 SubstWith l2) | ((S -termsOfMaxDepth) . nn)) | (SSS *) is Tnn -valued ;
then reconsider sXn = (l1 SubstWith l2) | Xn as AllTermsOf S -valued Function by RELAT_1:71;
A14: ( dom ((((l1,u) ReassignIn I) -TermEval) | X) = X & dom ((((l2,u) ReassignIn I) -TermEval) * sX) = X & dom ((((l2,u) ReassignIn I) -TermEval) * sXn) = Xn ) by PARTFUN1:def 2;
( rng ((((l1,u) ReassignIn I) -TermEval) | X) c= U & rng ((((l2,u) ReassignIn I) -TermEval) * sX) c= U ) by RELAT_1:def 19;
then reconsider f1 = (((l1,u) ReassignIn I) -TermEval) | X, f2 = (((l2,u) ReassignIn I) -TermEval) * sX as Function of X,U by FUNCT_2:2, A14;

now :: thesis: for x being object st x in X holds
f2 . x = f1 . x

let x be object ; :: thesis: ( x in X implies f2 . b₁ = f1 . b₁ )
assume A15: x in X ; :: thesis: f2 . b₁ = f1 . b₁
then reconsider XX = X as non empty Subset of TNN ;
reconsider xxx = x as Element of XX by A15;
reconsider xx = xxx as Element of SSS * by A15;
reconsider tN = x as Element of TNN by A15;
reconsider t = tN as NN -termal string of S by TARSKI:def 3, FOMODEL1:def 33;
reconsider ttt = t as Element of AllTermsOf S ;
set d = Depth t;
reconsider aux = rng xx as Subset of ((AllSymbolsOf S) \ {l2}) by RELAT_1:def 19;
( aux * c= SSS * & rng (SubTerms t) c= (rng t) * ) by RELAT_1:def 19;
then A16: rng (SubTerms t) c= SSS * by XBOOLE_1:1;
reconsider tt = t as nn + 1 -termal string of S ;
reconsider newt = (l1,l2) -SymbolSubstIn t as NN -termal string of S ;
A17: rng (SubTerms tt) c= (S -termsOfMaxDepth) . nn by RELAT_1:def 19;
A18: ( dom ((((l1,u) ReassignIn I) -TermEval) | Xn) = Xn & dom (((((l2,u) ReassignIn I) -TermEval) * (l1 SubstWith l2)) | Xn) = Xn ) by A14, RELAT_1:83, PARTFUN1:def 2;
( (f1 . xxx) \+\ ((((l1,u) ReassignIn I) -TermEval) . xxx) = {} & (((l1 SubstWith l2) | XX) . xxx) \+\ ((l1 SubstWith l2) . xxx) = {} & (((((l2,u) ReassignIn I) -TermEval) * sXX) . xxx) \+\ ((((l2,u) ReassignIn I) -TermEval) . (sXX . xxx)) = {} ) ;
then A19: ( f1 . x = (((l1,u) ReassignIn I) -TermEval) . x & sX . x = (l1 SubstWith l2) . x & f2 . x = (((l2,u) ReassignIn I) -TermEval) . (sX . x) ) by FOMODEL0:29;

per cases ( Depth t = 0 or Depth t <> 0 ) ;

suppose Depth t = 0 ; :: thesis: f2 . b₁ = f1 . b₁

then reconsider t0 = t as 0 -termal string of S by FOMODEL1:def 40;
reconsider l = (S -firstChar) . t0 as literal Element of S ;
A20: t0 = <*l*> ^ ((S -multiCat) . (SubTerms t0)) by FOMODEL1:def 37
.= <*l*> null {} ;
{(xx . 1)} \ SSS = {} ;
then t0 . 1 in SSS by ZFMISC_1:60;
then l in SSS by FOMODEL0:6;
then not l in dom (l2 .--> ({} .--> u)) by XBOOLE_0:def 5;
then A21: ((l2,u) ReassignIn I) . l = I . l by FUNCT_4:11;
A22: f1 . t0 = (((l1,u) ReassignIn I) . l) . ((((l1,u) ReassignIn I) -TermEval) * (SubTerms t0)) by FOMODEL2:21, A19
.= (((l1,u) ReassignIn I) . l) . {} ;

per cases ( l in dom (l1 .--> ({} .--> u)) or not l in dom (l1 .--> ({} .--> u)) ) ;

suppose A23: l in dom (l1 .--> ({} .--> u)) ; :: thesis: f2 . b₁ = f1 . b₁

l = l1 by A23, TARSKI:def 1;
then ( f1 . t0 = (((l1,u) ReassignIn I) . l1) . {} & (l1 SubstWith l2) . t0 = <*l2*> ) by A22, FOMODEL0:35, A20;
then f2 . t0 = (((l2,u) ReassignIn I) . ((S -firstChar) . <*l2*>)) . ((((l2,u) ReassignIn I) -TermEval) * (SubTerms <*l2*>)) by FOMODEL2:21, A19
.= (((l2,u) ReassignIn I) . (<*l2*> . 1)) . {} by FOMODEL0:6
.= (((l2,u) ReassignIn I) . l2) . {} ;
hence f2 . x = f1 . x by A23, TARSKI:def 1, A22, A1; :: thesis: verum

end;

suppose A24: not l in dom (l1 .--> ({} .--> u)) ; :: thesis: f2 . b₁ = f1 . b₁

then ( f1 . t0 = (I . l) . {} & not l in {l1} ) by A22, FUNCT_4:11;
then l <> l1 by TARSKI:def 1;
then (l1 SubstWith l2) . t0 = t0 by A20, FOMODEL0:35;
then f2 . t0 = (((l2,u) ReassignIn I) . l) . ((((l2,u) ReassignIn I) -TermEval) * (SubTerms t0)) by A19, FOMODEL2:21
.= (((l2,u) ReassignIn I) . l) . {} ;
hence f2 . x = f1 . x by A24, A22, FUNCT_4:11, A21; :: thesis: verum

end;

end;

end;

suppose Depth t <> 0 ; :: thesis: f2 . b₁ = f1 . b₁

then A25: not t is 0 -termal ;
then reconsider s1 = (S -firstChar) . t as non literal ofAtomicFormula Element of S by FOMODEL1:16;
( t . 1 = (S -firstChar) . t & not (S -firstChar) . t is literal ) by FOMODEL1:16, A25, FOMODEL0:6;
then newt . 1 = s1 by FUNCT_4:105;
then reconsider s2 = (S -firstChar) . newt as non literal ofAtomicFormula Element of S by FOMODEL0:6;
( not s1 in dom (l1 .--> ({} .--> u)) & not s2 in dom (l2 .--> ({} .--> u)) ) by TARSKI:def 1;
then A26: ( ((l1,u) ReassignIn I) . s1 = I . s1 & ((l2,u) ReassignIn I) . s2 = I . s2 ) by FUNCT_4:11;
s1 <> l1 ;
then t . 1 <> l1 by FOMODEL0:6;
then newt . 1 = t . 1 by FUNCT_4:105
.= s1 by FOMODEL0:6 ;
then A27: s1 = s2 by FOMODEL0:6;
thus f2 . x = (((l2,u) ReassignIn I) -TermEval) . newt by A19, FOMODEL0:def 22
.= (((l2,u) ReassignIn I) . s2) . ((((l2,u) ReassignIn I) -TermEval) * (SubTerms newt)) by FOMODEL2:21
.= (((l2,u) ReassignIn I) . s2) . ((((l2,u) ReassignIn I) -TermEval) * ((l1 SubstWith l2) * (SubTerms t))) by Lm38
.= (I . s2) . (((((l2,u) ReassignIn I) -TermEval) * (l1 SubstWith l2)) * (SubTerms t)) by A26, RELAT_1:36
.= (I . s2) . ((((((l2,u) ReassignIn I) -TermEval) * (l1 SubstWith l2)) | (((S -termsOfMaxDepth) . n) /\ (SSS *))) * (SubTerms t)) by RELAT_1:165, A17, A16, XBOOLE_1:19, A18
.= (I . s2) . ((((l1,u) ReassignIn I) -TermEval) * (SubTerms t)) by RELAT_1:165, A17, A16, XBOOLE_1:19, A18, A13
.= f1 . x by A19, A26, A27, FOMODEL2:21 ; :: thesis: verum

end;

end;

end;

then f1 = f2 by FUNCT_2:12;
hence S₁[n + 1] by RELAT_1:83; :: thesis: verum

end;

for m being Nat holds S₁[m] from NAT_1:sch 2(A2, A12);
hence (((l1,u) ReassignIn I) -TermEval) | ((((AllSymbolsOf S) \ {l2}) *) /\ ((S -termsOfMaxDepth) . m)) = ((((l2,u) ReassignIn I) -TermEval) * (l1 SubstWith l2)) | ((((AllSymbolsOf S) \ {l2}) *) /\ ((S -termsOfMaxDepth) . m)) ; :: thesis: verum