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;

now :: thesis: for x being object st x in Tm holds
((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;

hence for b₁ being Relation st b₁ = (l1 SubstWith l2) | ((S -termsOfMaxDepth) . m) holds
b₁ is (S -termsOfMaxDepth) . m -valued by FUNCT_2:3, A1; :: thesis: verum