set f = l1 SubstWith l2;
set SS = AllSymbolsOf S;
set TT = AllTermsOf S;
reconsider TTT = AllTermsOf S as non empty Subset of ((AllSymbolsOf S) *) by XBOOLE_1:1;
A1: dom ((l1 SubstWith l2) | TTT) = TTT by PARTFUN1:def 2;

let x be object ; :: thesis:
assume x in TTT ; :: thesis:
then reconsider tt = x as Element of TTT ;
reconsider t = tt as termal string of S by TARSKI:def 3;
(((l1 SubstWith l2) | TTT) . tt) \+\ ((l1 SubstWith l2) . tt) = {} ;
then ((l1 SubstWith l2) | TTT) . x = (l1 SubstWith l2) . t by FOMODEL0:29
.= (l1,l2) -SymbolSubstIn t by FOMODEL0:def 22 ;
hence ((l1 SubstWith l2) | TTT) . x in TTT by FOMODEL1:def 32; :: thesis:

end;