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 S1[ 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 ) );
A1: S1[ 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 A2: (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 A2, FOMODEL0:29;
then reconsider phii = phii as non 0wff wff exal string of S ;
A3: ((id (AllFormulasOf S)) . phiii) \+\ phiii = {} ;
not phii in dom (l AtomicSubst t) ;
then A4: (l Subst1 t) . phii = (id (AllFormulasOf S)) . phii by FUNCT_4:11
.= phii by A3 ;
reconsider tt = tail phii as empty set ;
thus (((l,t) Subst4 (l Subst1 t)) . 0) . phi = phi by Def22, A4; :: thesis: verum
end;
A5: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A6: S1[n] ; :: thesis: S1[n + 1]
then ( Depth phi <> (Depth phi) + (n + 1) & S1[n] ) ;
then A7: ( Depth phi <> ((Depth phi) + n) + 1 & S1[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 Lm44
.= (((l,t) Subst4 f) . (Depth phi)) . phi by A7, Def20 ; :: thesis: ( (S -firstChar) . phi = l implies (((l,t) Subst4 (l Subst1 t)) . (n + 1)) . phi = phi )
assume A8: (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 Lm44
.= phi by A6, A8, Def20 ; :: thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch 2(A1, A5);
 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