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;

now :: thesis: for x being object st x in TTT holds
((l1 SubstWith l2) | TTT) . x in TTT

let x be object ; :: thesis: ( x in TTT implies ((l1 SubstWith l2) | TTT) . x in TTT )
assume x in TTT ; :: thesis: ((l1 SubstWith l2) | TTT) . x in TTT
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: verum

end;

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