set s = l1 SubstWith l2;

set T = S -termsOfMaxDepth ;

set SS = AllSymbolsOf S;

reconsider Tm = (S -termsOfMaxDepth) . m as Subset of ((AllSymbolsOf S) *) by XBOOLE_1:1;

set f = (l1 SubstWith l2) | Tm;

A1: dom ((l1 SubstWith l2) | Tm) = Tm by PARTFUN1:def 2;

_{1} being Relation st b_{1} = (l1 SubstWith l2) | ((S -termsOfMaxDepth) . m) holds

b_{1} is (S -termsOfMaxDepth) . m -valued
by FUNCT_2:3, A1; :: thesis: verum

set T = S -termsOfMaxDepth ;

set SS = AllSymbolsOf S;

reconsider Tm = (S -termsOfMaxDepth) . m as Subset of ((AllSymbolsOf S) *) by XBOOLE_1:1;

set f = (l1 SubstWith l2) | Tm;

A1: dom ((l1 SubstWith l2) | Tm) = Tm by PARTFUN1:def 2;

now :: thesis: for x being object st x in Tm holds

((l1 SubstWith l2) | Tm) . x in (S -termsOfMaxDepth) . m

hence
for b((l1 SubstWith l2) | Tm) . x in (S -termsOfMaxDepth) . m

let x be object ; :: thesis: ( x in Tm implies ((l1 SubstWith l2) | Tm) . x in (S -termsOfMaxDepth) . m )

assume x in Tm ; :: thesis: ((l1 SubstWith l2) | Tm) . x in (S -termsOfMaxDepth) . m

then reconsider xx = x as Element of Tm ;

reconsider t = xx as m -termal string of S by TARSKI:def 3, FOMODEL1:def 33;

(((l1 SubstWith l2) | Tm) . xx) \+\ ((l1 SubstWith l2) . xx) = {} ;

then ((l1 SubstWith l2) | Tm) . x = (l1 SubstWith l2) . t by FOMODEL0:29

.= (l1,l2) -SymbolSubstIn t by FOMODEL0:def 22 ;

hence ((l1 SubstWith l2) | Tm) . x in (S -termsOfMaxDepth) . m by FOMODEL1:def 33; :: thesis: verum

end;assume x in Tm ; :: thesis: ((l1 SubstWith l2) | Tm) . x in (S -termsOfMaxDepth) . m

then reconsider xx = x as Element of Tm ;

reconsider t = xx as m -termal string of S by TARSKI:def 3, FOMODEL1:def 33;

(((l1 SubstWith l2) | Tm) . xx) \+\ ((l1 SubstWith l2) . xx) = {} ;

then ((l1 SubstWith l2) | Tm) . x = (l1 SubstWith l2) . t by FOMODEL0:29

.= (l1,l2) -SymbolSubstIn t by FOMODEL0:def 22 ;

hence ((l1 SubstWith l2) | Tm) . x in (S -termsOfMaxDepth) . m by FOMODEL1:def 33; :: thesis: verum

b