let m 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) Subst4 f) . ((Depth phi) + m)) . phi = (((l,t) Subst4 f) . (Depth phi)) . phi & ( (S -firstChar) . phi = l implies (((l,t) Subst4 (l Subst1 t)) . (Depth phi)) . phi = phi ) )
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) Subst4 f) . ((Depth phi) + m)) . phi = (((l,t) Subst4 f) . (Depth phi)) . phi & ( (S -firstChar) . phi = l implies (((l,t) Subst4 (l Subst1 t)) . (Depth phi)) . phi = phi ) )
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) Subst4 f) . ((Depth phi) + m)) . phi = (((l,t) Subst4 f) . (Depth phi)) . phi & ( (S -firstChar) . phi = l implies (((l,t) Subst4 (l Subst1 t)) . (Depth phi)) . phi = phi ) )
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) Subst4 f) . ((Depth phi) + m)) . phi = (((l,t) Subst4 f) . (Depth phi)) . phi & ( (S -firstChar) . phi = l implies (((l,t) Subst4 (l Subst1 t)) . (Depth phi)) . phi = phi ) )
let phi be wff string of S; :: thesis: for f being Element of Funcs ((AllFormulasOf S),(AllFormulasOf S)) holds
( (((l,t) Subst4 f) . ((Depth phi) + m)) . phi = (((l,t) Subst4 f) . (Depth phi)) . phi & ( (S -firstChar) . phi = l implies (((l,t) Subst4 (l Subst1 t)) . (Depth phi)) . phi = phi ) )
set TT = AllTermsOf S;
set FF = AllFormulasOf S;
set F = S -firstChar ;
let f be Element of Funcs ((AllFormulasOf S),(AllFormulasOf S)); :: thesis: ( (((l,t) Subst4 f) . ((Depth phi) + m)) . phi = (((l,t) Subst4 f) . (Depth phi)) . phi & ( (S -firstChar) . phi = l implies (((l,t) Subst4 (l Subst1 t)) . (Depth phi)) . phi = phi ) )
reconsider tt = t as Element of AllTermsOf S by FOMODEL1:def 32;
set f0 = l Subst1 t;
set f4 = (l,t) Subst4 (l Subst1 t);
set N = TheNorSymbOf S;
set L = LettersOf S;
set h = head phi;
set d = Depth phi;
set d1 = Depth (head phi);
set AF = AtomicFormulasOf S;
set f5 = (l,t) Subst4 f;
defpred S₁[ Nat] means ( (((l,t) Subst4 f) . ((Depth phi) + $1)) . phi = (((l,t) Subst4 f) . (Depth phi)) . phi & ( (S -firstChar) . phi = l implies (((l,t) Subst4 (l Subst1 t)) . $1) . phi = phi ) );
B0: S₁[ 0 ]

proof

thus (((l,t) Subst4 f) . ((Depth phi) + 0)) . phi = (((l,t) Subst4 f) . (Depth phi)) . phi ; :: thesis: ( (S -firstChar) . phi = l implies (((l,t) Subst4 (l Subst1 t)) . 0) . phi = phi )
assume C0: (S -firstChar) . phi = l ; :: thesis: (((l,t) Subst4 (l Subst1 t)) . 0) . phi = phi
then reconsider phii = phi as non 0wff wff string of S ;
reconsider phiii = phii as Element of AllFormulasOf S by FOMODEL2:16;
((S -firstChar) . phi) \+\ (TheNorSymbOf S) <> {} by C0, FOMODEL0:29;
then reconsider phii = phii as non 0wff wff exal string of S ;
C2: ((id (AllFormulasOf S)) . phiii) \+\ phiii = {} ;
not phii in dom (l AtomicSubst t) ;
then C3: (l Subst1 t) . phii = (id (AllFormulasOf S)) . phii by FUNCT_4:11
.= phii by C2, FOMODEL0:29 ;
reconsider tt = tail phii as empty set ;
thus (((l,t) Subst4 (l Subst1 t)) . 0) . phi = phi by DefSubst4, C3; :: thesis: verum

end;

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

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume ZZ0: S₁[n] ; :: thesis: S₁[n + 1]
then ( Depth phi <> (Depth phi) + (n + 1) & S₁[n] ) ;
then C0: ( Depth phi <> ((Depth phi) + n) + 1 & S₁[n] ) ;
thus (((l,t) Subst4 f) . ((Depth phi) + (n + 1))) . phi = (((l,t) Subst4 f) . (((Depth phi) + n) + 1)) . phi
.= (l,t,((Depth phi) + n),(((l,t) Subst4 f) . ((Depth phi) + n))) Subst2 phi by Lm48
.= (((l,t) Subst4 f) . (Depth phi)) . phi by C0, DefSubst2 ; :: thesis: ( (S -firstChar) . phi = l implies (((l,t) Subst4 (l Subst1 t)) . (n + 1)) . phi = phi )
assume C2: (S -firstChar) . phi = l ; :: thesis: (((l,t) Subst4 (l Subst1 t)) . (n + 1)) . phi = phi
then ( ((S -firstChar) . phi) \+\ (TheNorSymbOf S) <> {} & not phi is 0 -wff ) by FOMODEL0:29;
then ( not phi is 0wff & ( phi is exal or phi is 0wff ) ) ;
then reconsider phii = phi as non 0wff wff exal string of S ;
thus (((l,t) Subst4 (l Subst1 t)) . (n + 1)) . phi = (l,t,n,(((l,t) Subst4 (l Subst1 t)) . n)) Subst2 phii by Lm48
.= phi by ZZ0, C2, DefSubst2 ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(B0, B1);
hence ( (((l,t) Subst4 f) . ((Depth phi) + m)) . phi = (((l,t) Subst4 f) . (Depth phi)) . phi & ( (S -firstChar) . phi = l implies (((l,t) Subst4 (l Subst1 t)) . (Depth phi)) . phi = phi ) ) ; :: thesis: verum