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 st phi is m -wff holds
(l,t) SubstIn phi = (((l,t) Subst4 (l Subst1 t)) . m) . 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 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: (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 ; :: thesis: verum