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 ;

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 )
;

end;

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;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

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;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

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;hence (l,t,n,f) Subst2 phi is wff string of S by TARSKI:def 3; :: thesis: verum

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;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