let S be Language; :: thesis: for l1, l2 being literal Element of S
for psi1 being wff string of S ex psi2 being wff string of S st
( Depth psi1 = Depth psi2 & (l1 SubstWith l2) . psi1 = psi2 )
let l1, l2 be literal Element of S; :: thesis: for psi1 being wff string of S ex psi2 being wff string of S st
( Depth psi1 = Depth psi2 & (l1 SubstWith l2) . psi1 = psi2 )
let psi1 be wff string of S; :: thesis: ex psi2 being wff string of S st
( Depth psi1 = Depth psi2 & (l1 SubstWith l2) . psi1 = psi2 )
set e = l1 SubstWith l2;
set N = TheNorSymbOf S;
set L = LettersOf S;
defpred S₁[ wff string of S] means ex psi being wff string of S st
( Depth psi = Depth $1 & (l1 SubstWith l2) . $1 = psi );
defpred S₂[ Nat] means for phi being wff string of S st Depth phi <= $1 holds
S₁[phi];
A1: S₂[ 0 ]

proof

thus for phi being wff string of S st Depth phi <= 0 holds
S₁[phi] :: thesis: verum

proof

let phi be wff string of S; :: thesis: ( Depth phi <= 0 implies S₁[phi] )
set D = Depth phi;
assume Depth phi <= 0 ; :: thesis: S₁[phi]
then Depth phi = 0 ;
then reconsider p0 = phi as 0 -wff string of S by FOMODEL2:def 31;
reconsider psi = (l1,l2) -SymbolSubstIn p0 as 0wff string of S ;
take psi ; :: thesis: ( Depth psi = Depth phi & (l1 SubstWith l2) . phi = psi )
thus Depth psi = Depth phi ; :: thesis: (l1 SubstWith l2) . phi = psi
thus (l1 SubstWith l2) . phi = psi by FOMODEL0:def 22; :: thesis: verum

end;

end;

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

proof

let n be Nat; :: thesis: ( S₂[n] implies S₂[n + 1] )
set Fn = S -formulasOfMaxDepth n;
assume A3: S₂[n] ; :: thesis: S₂[n + 1]
thus for phi being wff string of S st Depth phi <= n + 1 holds
S₁[phi] :: thesis: verum

proof

let phi be wff string of S; :: thesis: ( Depth phi <= n + 1 implies S₁[phi] )
set D = Depth phi;
assume A4: Depth phi <= n + 1 ; :: thesis: S₁[phi]

per cases ( phi is 0wff or phi is exal or ( not phi is exal & not phi is 0wff ) ) ;

suppose phi is 0wff ; :: thesis: S₁[phi]

then reconsider p0 = phi as 0wff string of S ;
reconsider psi = (l1,l2) -SymbolSubstIn p0 as 0wff string of S ;
take psi ; :: thesis: ( Depth psi = Depth phi & (l1 SubstWith l2) . phi = psi )
thus Depth psi = Depth phi ; :: thesis: (l1 SubstWith l2) . phi = psi
thus (l1 SubstWith l2) . phi = psi by FOMODEL0:def 22; :: thesis: verum

end;

suppose A5: phi is exal ; :: thesis: S₁[phi]

then consider m being Nat such that
A6: Depth phi = m + 1 by NAT_1:6;
phi in m -ExFormulasOf S by A6, A5, FOMODEL2:18;
then consider v being Element of LettersOf S, phi1 being Element of S -formulasOfMaxDepth m such that
A7: phi = <*v*> ^ phi1 ;
reconsider l = v as literal Element of S ;
reconsider phi11 = phi1 as m -wff string of S by FOMODEL2:def 24;
set m1 = Depth phi11;
(Depth phi11) + 1 <= n + 1 by A4, A7, FOMODEL2:17;
then consider psi1 being wff string of S such that
A8: ( Depth psi1 = Depth phi11 & (l1 SubstWith l2) . phi11 = psi1 ) by A3, XREAL_1:8;
( l = l1 or l <> l1 ) ;
then ( (l1 SubstWith l2) . <*l*> = <*l2*> or (l1 SubstWith l2) . <*l*> = <*l*> ) by FOMODEL0:35;
then consider s being literal Element of S such that
A9: (l1 SubstWith l2) . <*l*> = <*s*> ;
take psi = <*s*> ^ psi1; :: thesis: ( Depth psi = Depth phi & (l1 SubstWith l2) . phi = psi )
thus Depth psi = (Depth psi1) + 1 by FOMODEL2:17
.= Depth phi by A8, A7, FOMODEL2:17 ; :: thesis: (l1 SubstWith l2) . phi = psi
thus (l1 SubstWith l2) . phi = psi by A9, A8, A7, FOMODEL0:36; :: thesis: verum

end;

suppose A10: ( not phi is exal & not phi is 0wff ) ; :: thesis: S₁[phi]

then consider m being Nat such that
A11: Depth phi = m + 1 by NAT_1:6;
phi in m -NorFormulasOf S by FOMODEL2:18, A10, A11;
then consider phi1, phi2 being Element of S -formulasOfMaxDepth m such that
A12: phi = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 ;
reconsider phi11 = phi1, phi22 = phi2 as m -wff string of S by FOMODEL2:def 24;
set m1 = Depth phi11;
set m2 = Depth phi22;
set M = max ((Depth phi11),(Depth phi22));
A13: ( ((max ((Depth phi11),(Depth phi22))) - (Depth phi11)) + (Depth phi11) >= 0 + (Depth phi11) & ((max ((Depth phi11),(Depth phi22))) - (Depth phi22)) + (Depth phi22) >= 0 + (Depth phi22) ) by XREAL_1:6;
n + 1 >= (max ((Depth phi11),(Depth phi22))) + 1 by FOMODEL2:17, A4, A12;
then n >= max ((Depth phi11),(Depth phi22)) by XREAL_1:8;
then ( S₁[phi11] & S₁[phi22] ) by A3, A13, XXREAL_0:2;
then consider psi1, psi2 being wff string of S such that
A14: ( Depth psi1 = Depth phi11 & (l1 SubstWith l2) . phi11 = psi1 & Depth psi2 = Depth phi22 & (l1 SubstWith l2) . phi22 = psi2 ) ;
take psi = (<*(TheNorSymbOf S)*> ^ psi1) ^ psi2; :: thesis: ( Depth psi = Depth phi & (l1 SubstWith l2) . phi = psi )
thus Depth phi = (max ((Depth phi11),(Depth phi22))) + 1 by A12, FOMODEL2:17
.= Depth psi by A14, FOMODEL2:17 ; :: thesis: (l1 SubstWith l2) . phi = psi
thus (l1 SubstWith l2) . phi = ((l1 SubstWith l2) . (<*(TheNorSymbOf S)*> ^ phi11)) ^ ((l1 SubstWith l2) . phi22) by A12, FOMODEL0:36
.= (((l1 SubstWith l2) . <*(TheNorSymbOf S)*>) ^ ((l1 SubstWith l2) . phi11)) ^ psi2 by A14, FOMODEL0:36
.= psi by FOMODEL0:35, A14 ; :: thesis: verum

end;

end;

end;

end;

for n being Nat holds S₂[n] from NAT_1:sch 2(A1, A2);
hence ex psi2 being wff string of S st
( Depth psi1 = Depth psi2 & (l1 SubstWith l2) . psi1 = psi2 ) ; :: thesis: verum