let U be non empty set ; :: thesis:
let u1 be Element of U; :: thesis:
let S be Language; :: thesis:
let l1, l2 be literal Element of S; :: thesis:
let psi be wff string of S; :: thesis:
set II = U -InterpretersOf S;
set s = l1 SubstWith l2;
set SS = AllSymbolsOf S;
set SSS = (AllSymbolsOf S) \ {l2};
set TT = AllTermsOf S;
set T = S -termsOfMaxDepth ;
set F = S -firstChar ;
set N = TheNorSymbOf S;
reconsider SSSS = (AllSymbolsOf S) \ {l2} as non empty Subset of (AllSymbolsOf S) ;
defpred S₁[ Nat] means for I being Element of U -InterpretersOf S
for u being Element of U
for phi being wff string of S st phi is $1 -wff & phi is (AllSymbolsOf S) \ {l2} -valued holds
((l1,u) ReassignIn I) -TruthEval phi = ((l2,u) ReassignIn I) -TruthEval ((l1,l2) -SymbolSubstIn phi);
A1: S₁[ 0 ]

let I be Element of U -InterpretersOf S; :: thesis:
let u be Element of U; :: thesis:
let phi be wff string of S; :: thesis:
set I1 = (l1,u) ReassignIn I;
set I2 = (l2,u) ReassignIn I;
assume phi is 0 -wff ; :: thesis:
then reconsider phi0 = phi as 0wff string of S ;
assume phi is (AllSymbolsOf S) \ {l2} -valued ; :: thesis:
then ((l1,u) ReassignIn I) -TruthEval phi0 = ((l2,u) ReassignIn I) -TruthEval ((l1,l2) -SymbolSubstIn phi0) by Lm41;
hence ((l1,u) ReassignIn I) -TruthEval phi = ((l2,u) ReassignIn I) -TruthEval ((l1,l2) -SymbolSubstIn phi) ; :: thesis:

end;

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

let n be Nat; :: thesis:
assume A3: S₁[n] ; :: thesis:
let I be Element of U -InterpretersOf S; :: thesis:
let u be Element of U; :: thesis:
let phi be wff string of S; :: thesis:
set I1 = (l1,u) ReassignIn I;
set I2 = (l2,u) ReassignIn I;
assume A4: ( phi is n + 1 -wff & phi is (AllSymbolsOf S) \ {l2} -valued ) ; :: thesis:
then reconsider phii = phi as n + 1 -wff string of S ;
reconsider x = phi as non empty SSSS -valued FinSequence by A4;
{(x . 1)} \ ((AllSymbolsOf S) \ {l2}) = {} ;
then phii . 1 in (AllSymbolsOf S) \ {l2} by ZFMISC_1:60;
then (S -firstChar) . phii in (AllSymbolsOf S) \ {l2} by FOMODEL0:6;
then not (S -firstChar) . phii in {l2} by XBOOLE_0:def 5;
then A5: (S -firstChar) . phii <> l2 by TARSKI:def 1;
reconsider psi = (l1,l2) -SymbolSubstIn phii as n + 1 -wff string of S ;
reconsider phi1 = head phii as n -wff string of S ;
reconsider psi1 = (l1,l2) -SymbolSubstIn phi1 as n -wff string of S ;

suppose ( phi is exal & not phi is 0wff ) ; :: thesis:

then reconsider phii = phii as non 0wff n + 1 -wff exal string of S ;
set l = (S -firstChar) . phii;
set phi2 = tail phii;
A6: phii = (<*((S -firstChar) . phii)*> ^ phi1) ^ (tail phii) by FOMODEL2:23
.= <*((S -firstChar) . phii)*> ^ phi1 ;
then (l1 SubstWith l2) . phii = ((l1 SubstWith l2) . <*((S -firstChar) . phii)*>) ^ ((l1 SubstWith l2) . phi1) by FOMODEL0:36
.= ((l1 SubstWith l2) . <*((S -firstChar) . phii)*>) ^ psi1 by FOMODEL0:def 22 ;
then A7: psi = ((l1 SubstWith l2) . <*((S -firstChar) . phii)*>) ^ psi1 by FOMODEL0:def 22;
x = (<*((S -firstChar) . phii)*> ^ phi1) ^ {} by A6;
then A8: phi1 is SSSS -valued by FOMODEL0:44;
( ((l1,u) ReassignIn I) -TruthEval phii = 1 iff ((l2,u) ReassignIn I) -TruthEval psi = 1 )

per cases ) . phii = l1 or (S -firstChar) . phii <> l1 ) ;

suppose A9: (S -firstChar) . phii = l1 ; :: thesis:

then A10: psi = <*l2*> ^ psi1 by A7, FOMODEL0:35;

hereby :: thesis:

assume ((l1,u) ReassignIn I) -TruthEval phii = 1 ; :: thesis:
then consider u1 being Element of U such that
A11: ((((S -firstChar) . phii),u1) ReassignIn ((l1,u) ReassignIn I)) -TruthEval phi1 = 1 by A6, FOMODEL2:19;
1 = ((l1,u1) ReassignIn I) -TruthEval phi1 by A11, A9, FOMODEL0:43
.= ((l2,u1) ReassignIn I) -TruthEval psi1 by A8, A3
.= ((l2,u1) ReassignIn ((l2,u) ReassignIn I)) -TruthEval psi1 by FOMODEL0:43 ;
hence ((l2,u) ReassignIn I) -TruthEval psi = 1 by A10, FOMODEL2:19; :: thesis:

end;

assume ((l2,u) ReassignIn I) -TruthEval psi = 1 ; :: thesis:
then consider u2 being Element of U such that
A12: ((l2,u2) ReassignIn ((l2,u) ReassignIn I)) -TruthEval psi1 = 1 by A10, FOMODEL2:19;
1 = ((l2,u2) ReassignIn I) -TruthEval psi1 by A12, FOMODEL0:43
.= ((l1,u2) ReassignIn I) -TruthEval phi1 by A8, A3
.= ((((S -firstChar) . phii),u2) ReassignIn ((l1,u) ReassignIn I)) -TruthEval phi1 by A9, FOMODEL0:43 ;
hence ((l1,u) ReassignIn I) -TruthEval phii = 1 by A6, FOMODEL2:19; :: thesis:

end;

suppose A13: (S -firstChar) . phii <> l1 ; :: thesis:

then A14: psi = <*((S -firstChar) . phii)*> ^ psi1 by A7, FOMODEL0:35;

hereby :: thesis:

assume ((l1,u) ReassignIn I) -TruthEval phii = 1 ; :: thesis:
then consider u1 being Element of U such that
A15: ((((S -firstChar) . phii),u1) ReassignIn ((l1,u) ReassignIn I)) -TruthEval phi1 = 1 by A6, FOMODEL2:19;
1 = ((l1,u) ReassignIn ((((S -firstChar) . phii),u1) ReassignIn I)) -TruthEval phi1 by A15, A13, FOMODEL0:43
.= ((l2,u) ReassignIn ((((S -firstChar) . phii),u1) ReassignIn I)) -TruthEval psi1 by A3, A8
.= ((((S -firstChar) . phii),u1) ReassignIn ((l2,u) ReassignIn I)) -TruthEval psi1 by A5, FOMODEL0:43 ;
hence ((l2,u) ReassignIn I) -TruthEval psi = 1 by A14, FOMODEL2:19; :: thesis:

end;

assume ((l2,u) ReassignIn I) -TruthEval psi = 1 ; :: thesis:
then consider u2 being Element of U such that
A16: ((((S -firstChar) . phii),u2) ReassignIn ((l2,u) ReassignIn I)) -TruthEval psi1 = 1 by A14, FOMODEL2:19;
1 = ((l2,u) ReassignIn ((((S -firstChar) . phii),u2) ReassignIn I)) -TruthEval psi1 by A5, A16, FOMODEL0:43
.= ((l1,u) ReassignIn ((((S -firstChar) . phii),u2) ReassignIn I)) -TruthEval phi1 by A3, A8
.= ((((S -firstChar) . phii),u2) ReassignIn ((l1,u) ReassignIn I)) -TruthEval phi1 by A13, FOMODEL0:43 ;
hence ((l1,u) ReassignIn I) -TruthEval phii = 1 by A6, FOMODEL2:19; :: thesis:

end;

end;

end;

then ( ((l1,u) ReassignIn I) -TruthEval phii = 1 iff not ((l2,u) ReassignIn I) -TruthEval psi = 0 ) by FOMODEL0:39;
hence ((l1,u) ReassignIn I) -TruthEval phi = ((l2,u) ReassignIn I) -TruthEval ((l1,l2) -SymbolSubstIn phi) by FOMODEL0:39; :: thesis:

end;

suppose ( not phi is exal & not phi is 0wff ) ; :: thesis:

then reconsider phii = phii as non 0wff n + 1 -wff non exal string of S ;
reconsider phi2 = tail phii as n -wff string of S ;
reconsider psi2 = (l1,l2) -SymbolSubstIn phi2 as n -wff string of S ;
((S -firstChar) . phii) \+\ (TheNorSymbOf S) = {} ;
then (S -firstChar) . phii = TheNorSymbOf S by FOMODEL0:29;
then A17: phii = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 by FOMODEL2:23;
then ( phi1 is (AllSymbolsOf S) \ {l2} -valued & phi2 is (AllSymbolsOf S) \ {l2} -valued & ( ((l1,u) ReassignIn I) -TruthEval phii = 1 implies ( ((l1,u) ReassignIn I) -TruthEval phi1 = 0 & ((l1,u) ReassignIn I) -TruthEval phi2 = 0 ) ) & ( ((l1,u) ReassignIn I) -TruthEval phi1 = 0 & ((l1,u) ReassignIn I) -TruthEval phi2 = 0 implies ((l1,u) ReassignIn I) -TruthEval phii = 1 ) ) by A4, FOMODEL0:44, FOMODEL2:19;
then A18: ( ((l1,u) ReassignIn I) -TruthEval phii = 1 iff ( ((l2,u) ReassignIn I) -TruthEval psi1 = 0 & ((l2,u) ReassignIn I) -TruthEval psi2 = 0 ) ) by A3;
A19: ( (l1 SubstWith l2) . phii = psi & (l1 SubstWith l2) . phi1 = psi1 & (l1 SubstWith l2) . phi2 = psi2 ) by FOMODEL0:def 22;
then psi = ((l1 SubstWith l2) . (<*(TheNorSymbOf S)*> ^ phi1)) ^ ((l1 SubstWith l2) . phi2) by A17, FOMODEL0:36
.= (((l1 SubstWith l2) . <*(TheNorSymbOf S)*>) ^ ((l1 SubstWith l2) . phi1)) ^ ((l1 SubstWith l2) . phi2) by FOMODEL0:36
.= (<*(TheNorSymbOf S)*> ^ psi1) ^ psi2 by FOMODEL0:35, A19 ;
then ( ((l2,u) ReassignIn I) -TruthEval psi = 1 iff not ((l1,u) ReassignIn I) -TruthEval phi = 0 ) by FOMODEL0:39, FOMODEL2:19, A18;
hence ((l1,u) ReassignIn I) -TruthEval phi = ((l2,u) ReassignIn I) -TruthEval ((l1,l2) -SymbolSubstIn phi) by FOMODEL0:39; :: thesis:

end;

suppose phi is 0 -wff ; :: thesis:

hence ((l1,u) ReassignIn I) -TruthEval phi = ((l2,u) ReassignIn I) -TruthEval ((l1,l2) -SymbolSubstIn phi) by A1, A4; :: thesis:

end;

end;

end;

A20: for m being Nat holds S₁[m] from NAT_1:sch 2(A1, A2);
set m = Depth psi;
assume not l2 in rng psi ; :: thesis:
then ( {l2} misses rng psi & rng psi c= AllSymbolsOf S ) by RELAT_1:def 19, ZFMISC_1:50;
then A21: ( psi is Depth psi -wff & psi is (AllSymbolsOf S) \ {l2} -valued ) by XBOOLE_1:86, FOMODEL2:def 31, RELAT_1:def 19;
let I be Element of U -InterpretersOf S; :: thesis:
thus ((l1,u1) ReassignIn I) -TruthEval psi = ((l2,u1) ReassignIn I) -TruthEval ((l1,l2) -SymbolSubstIn psi) by A20, A21; :: thesis: