let m be Nat; 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 st phi is m -wff holds
(l,t) SubstIn phi = (((l,t) Subst4 (l Subst1 t)) . m) . phi
let S be Language; for l being literal Element of S
for t being termal string of S
for phi being wff string of S st phi is m -wff holds
(l,t) SubstIn phi = (((l,t) Subst4 (l Subst1 t)) . m) . phi
let l be literal Element of S; for t being termal string of S
for phi being wff string of S st phi is m -wff holds
(l,t) SubstIn phi = (((l,t) Subst4 (l Subst1 t)) . m) . phi
let t be termal string of S; for phi being wff string of S st phi is m -wff holds
(l,t) SubstIn phi = (((l,t) Subst4 (l Subst1 t)) . m) . phi
let phi be wff string of S; ( phi is m -wff implies (l,t) SubstIn phi = (((l,t) Subst4 (l Subst1 t)) . m) . phi )
set d = Depth phi;
set FF = AllFormulasOf S;
reconsider f = l Subst1 t as Element of Funcs ((AllFormulasOf S),(AllFormulasOf S)) ;
assume
phi is m -wff
; (l,t) SubstIn phi = (((l,t) Subst4 (l Subst1 t)) . m) . phi
then reconsider k = m - (Depth phi) as Nat ;
(((l,t) Subst4 f) . ((Depth phi) + k)) . phi = (l,t) SubstIn phi
by Lm45;
hence
(l,t) SubstIn phi = (((l,t) Subst4 (l Subst1 t)) . m) . phi
; verum