let S be Language; :: thesis: for l1, l2 being literal Element of S holds (l1 SubstWith l2) | (AllTermsOf S) is Function of (AllTermsOf S),(AllTermsOf S)
let l1, l2 be literal Element of S; :: thesis: (l1 SubstWith l2) | (AllTermsOf S) is Function of (AllTermsOf S),(AllTermsOf S)
set e = l1 SubstWith l2;
set SS = AllSymbolsOf S;
set TT = AllTermsOf S;
(AllTermsOf S) /\ (((AllSymbolsOf S) *) \ {{}}) = (AllTermsOf S) null (((AllSymbolsOf S) *) \ {{}})
.= AllTermsOf S ;
then reconsider TTT = AllTermsOf S as non empty Subset of ((AllSymbolsOf S) *) ;
set f = (l1 SubstWith l2) | TTT;
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 A2: x in TTT ; :: thesis: ((l1 SubstWith l2) | TTT) . x in TTT
then reconsider t = x as termal string of S ;
reconsider xx = x as Element of TTT by A2;
(((l1 SubstWith l2) | TTT) . xx) \+\ ((l1 SubstWith l2) . xx) = {} ;
then ((l1 SubstWith l2) | TTT) . xx = (l1 SubstWith l2) . xx 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 (l1 SubstWith l2) | (AllTermsOf S) is Function of (AllTermsOf S),(AllTermsOf S) by FUNCT_2:3, A1; :: thesis: verum