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;

_{1} being Relation st b_{1} = (l1 SubstWith l2) | (AllTermsOf S) holds

b_{1} is AllTermsOf S -valued
by A1, FUNCT_2:3; :: thesis: verum

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

hence
for b((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;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

b