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) . (m + 1)) . phi = (l,t,m,(((l,t) Subst4 f) . m)) Subst2 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) . (m + 1)) . phi = (l,t,m,(((l,t) Subst4 f) . m)) Subst2 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) . (m + 1)) . phi = (l,t,m,(((l,t) Subst4 f) . m)) Subst2 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) . (m + 1)) . phi = (l,t,m,(((l,t) Subst4 f) . m)) Subst2 phi
let phi be wff string of S; :: thesis: for f being Element of Funcs ((AllFormulasOf S),(AllFormulasOf S)) holds (((l,t) Subst4 f) . (m + 1)) . phi = (l,t,m,(((l,t) Subst4 f) . m)) Subst2 phi
set FF = AllFormulasOf S;
set D = Funcs ((AllFormulasOf S),(AllFormulasOf S));
let f be Element of Funcs ((AllFormulasOf S),(AllFormulasOf S)); :: thesis: (((l,t) Subst4 f) . (m + 1)) . phi = (l,t,m,(((l,t) Subst4 f) . m)) Subst2 phi
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
set f4 = (l,t) Subst4 f;
set f3 = (l,t,m,(((l,t) Subst4 f) . mm)) Subst3 ;
(((l,t) Subst4 f) . (mm + 1)) . phi = ((l,t,m,(((l,t) Subst4 f) . mm)) Subst3) . phi by DefSubst4
.= (l,t,m,(((l,t) Subst4 f) . mm)) Subst2 phi by DefSubst3 ;
hence (((l,t) Subst4 f) . (m + 1)) . phi = (l,t,m,(((l,t) Subst4 f) . m)) Subst2 phi ; :: thesis: verum