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

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