let S be Language; :: thesis: for l1, l2 being literal Element of S
for psi1 being wff string of S holds Depth psi1 = Depth ((l1,l2) -SymbolSubstIn psi1)
let l1, l2 be literal Element of S; :: thesis: for psi1 being wff string of S holds Depth psi1 = Depth ((l1,l2) -SymbolSubstIn psi1)
let psi1 be wff string of S; :: thesis: Depth psi1 = Depth ((l1,l2) -SymbolSubstIn psi1)
set e = l1 SubstWith l2;
set psi = (l1,l2) -SymbolSubstIn psi1;
consider psi2 being wff string of S such that
A1: ( Depth psi2 = Depth psi1 & psi2 = (l1 SubstWith l2) . psi1 ) by Lm33;
thus Depth psi1 = Depth ((l1,l2) -SymbolSubstIn psi1) by A1, FOMODEL0:def 22; :: thesis: verum