let n be Nat; :: thesis: for S being Language
for l being literal Element of S
for t being termal string of S
for phi being wff string of S
for f being Element of Funcs ((AllFormulasOf S),(AllFormulasOf S)) holds (l,t,n,f) Subst2 phi is wff string of S
let S be Language; :: thesis: for l being literal Element of S
for t being termal string of S
for phi being wff string of S
for f being Element of Funcs ((AllFormulasOf S),(AllFormulasOf S)) holds (l,t,n,f) Subst2 phi is wff string of S
let l be literal Element of S; :: thesis: for t being termal string of S
for phi being wff string of S
for f being Element of Funcs ((AllFormulasOf S),(AllFormulasOf S)) holds (l,t,n,f) Subst2 phi is wff string of S
let t be termal string of S; :: thesis: for phi being wff string of S
for f being Element of Funcs ((AllFormulasOf S),(AllFormulasOf S)) holds (l,t,n,f) Subst2 phi is wff string of S
let phi be wff string of S; :: thesis: for f being Element of Funcs ((AllFormulasOf S),(AllFormulasOf S)) holds (l,t,n,f) Subst2 phi is wff string of S
set FF = AllFormulasOf S;
set h = head phi;
set d = Depth phi;
set F = S -firstChar ;
let f be Element of Funcs ((AllFormulasOf S),(AllFormulasOf S)); :: thesis: (l,t,n,f) Subst2 phi is wff string of S
reconsider ff = f as Function of (AllFormulasOf S),(AllFormulasOf S) ;
set IT = (l,t,n,f) Subst2 phi;
set N = TheNorSymbOf S;
set L = LettersOf S;
set X = (LettersOf S) \ (((rng t) \/ (rng (head phi))) \/ {l});
set ll1 = the Element of (LettersOf S) \ (((rng t) \/ (rng (head phi))) \/ {l});
reconsider hh = head phi, phii = phi as Element of AllFormulasOf S by FOMODEL2:16;
reconsider newhead = ff . hh as wff string of S by TARSKI:def 3;
reconsider XX = (LettersOf S) \ (((rng t) \/ (rng (head phi))) \/ {l}) as non empty Subset of (LettersOf S) ;
the Element of (LettersOf S) \ (((rng t) \/ (rng (head phi))) \/ {l}) is Element of XX ;
then reconsider l1 = the Element of (LettersOf S) \ (((rng t) \/ (rng (head phi))) \/ {l}) as literal Element of S ;

per cases ( ( Depth phi = n + 1 & not phi is exal ) or ( Depth phi = n + 1 & phi is exal & (S -firstChar) . phi <> l ) or Depth phi <> n + 1 or (S -firstChar) . phi = l ) ;

suppose A1: ( Depth phi = n + 1 & not phi is exal ) ; :: thesis: (l,t,n,f) Subst2 phi is wff string of S

then not phi is 0 -wff ;
then reconsider phiii = phi as non 0wff wff non exal string of S by A1;
reconsider ttt = tail phiii as wff string of S ;
reconsider tt = ttt as Element of AllFormulasOf S by FOMODEL2:16;
reconsider newtail = ff . tt as wff string of S by TARSKI:def 3;
(l,t,n,f) Subst2 phi = (<*(TheNorSymbOf S)*> ^ newhead) ^ newtail by A1, Def20;
hence (l,t,n,f) Subst2 phi is wff string of S ; :: thesis: verum

end;

suppose A2: ( Depth phi = n + 1 & phi is exal & (S -firstChar) . phi <> l ) ; :: thesis: (l,t,n,f) Subst2 phi is wff string of S

reconsider phiii = phi as non 0wff wff exal string of S by A2;
reconsider l = (S -firstChar) . phiii as literal Element of S ;
reconsider newhead = (l,l1) -SymbolSubstIn (head phi) as wff string of S ;
reconsider newheadd = newhead as Element of AllFormulasOf S by FOMODEL2:16;
reconsider newesthead = ff . newheadd as wff string of S by TARSKI:def 3;
(l,t,n,f) Subst2 phi = <*l1*> ^ newesthead by A2, Def20;
hence (l,t,n,f) Subst2 phi is wff string of S ; :: thesis: verum

end;

suppose Depth phi <> n + 1 ; :: thesis: (l,t,n,f) Subst2 phi is wff string of S

then (l,t,n,f) Subst2 phi = ff . phii by Def20;
hence (l,t,n,f) Subst2 phi is wff string of S by TARSKI:def 3; :: thesis: verum

end;

suppose (S -firstChar) . phi = l ; :: thesis: (l,t,n,f) Subst2 phi is wff string of S

then ( (S -firstChar) . phi = l & phi is exal ) ;
then (l,t,n,f) Subst2 phi = ff . phii by Def20;
hence (l,t,n,f) Subst2 phi is wff string of S by TARSKI:def 3; :: thesis: verum

end;

end;