let S be Language; :: thesis: for l1, l2 being literal Element of S
for t being termal string of S holds SubTerms ((l1,l2) -SymbolSubstIn t) = (l1 SubstWith l2) * (SubTerms t)
let l1, l2 be literal Element of S; :: thesis: for t being termal string of S holds SubTerms ((l1,l2) -SymbolSubstIn t) = (l1 SubstWith l2) * (SubTerms t)
let t be termal string of S; :: thesis: SubTerms ((l1,l2) -SymbolSubstIn t) = (l1 SubstWith l2) * (SubTerms t)
set s = l1 SubstWith l2;
set newt = (l1,l2) -SymbolSubstIn t;
set ST = SubTerms t;
set F = S -firstChar ;
set C = S -multiCat ;
set ST2 = SubTerms ((l1,l2) -SymbolSubstIn t);
set SS = AllSymbolsOf S;
set TT = AllTermsOf S;
reconsider TTT = AllTermsOf S as Subset of ((AllSymbolsOf S) *) by XBOOLE_1:1;
A1: ( rng (SubTerms t) c= AllTermsOf S & dom ((l1 SubstWith l2) | TTT) = TTT & rng ((l1 SubstWith l2) | (AllTermsOf S)) c= AllTermsOf S ) by RELAT_1:def 19, PARTFUN1:def 2;
then reconsider ss = (l1 SubstWith l2) | (AllTermsOf S) as Function of (AllTermsOf S),(AllTermsOf S) by FUNCT_2:2;

per cases ( not t is 0 -termal or t is 0 -termal ) ;

suppose not t is 0 -termal ; :: thesis: SubTerms ((l1,l2) -SymbolSubstIn t) = (l1 SubstWith l2) * (SubTerms t)

then reconsider s1 = (S -firstChar) . t as non literal ofAtomicFormula Element of S by FOMODEL1:16;
reconsider h = (l1,l2) -SymbolSubstIn <*s1*> as AllSymbolsOf S -valued 1 -element FinSequence ;
set s2 = (S -firstChar) . ((l1,l2) -SymbolSubstIn t);
set n1 = |.(ar s1).|;
set n2 = |.(ar ((S -firstChar) . ((l1,l2) -SymbolSubstIn t))).|;
ss * (SubTerms t) = (l1 SubstWith l2) * (SubTerms t) by RELAT_1:165, A1;
then reconsider p = (l1 SubstWith l2) * (SubTerms t) as |.(ar s1).| -element FinSequence of AllTermsOf S by FOMODEL0:26;
A2: (l1,l2) -SymbolSubstIn t = <*((S -firstChar) . ((l1,l2) -SymbolSubstIn t))*> ^ ((S -multiCat) . (SubTerms ((l1,l2) -SymbolSubstIn t))) by FOMODEL1:def 37;
t = <*s1*> ^ ((S -multiCat) . (SubTerms t)) by FOMODEL1:def 37;
then (l1 SubstWith l2) . t = ((l1 SubstWith l2) . <*s1*>) ^ ((l1 SubstWith l2) . ((S -multiCat) . (SubTerms t))) by FOMODEL0:36
.= h ^ ((l1 SubstWith l2) . ((S -multiCat) . (SubTerms t))) by FOMODEL0:def 22
.= h ^ ((S -multiCat) . ((l1 SubstWith l2) * (SubTerms t))) by FOMODEL0:37 ;
then A3: (l1,l2) -SymbolSubstIn t = h ^ ((S -multiCat) . p) by FOMODEL0:def 22;
then ( h = <*((S -firstChar) . ((l1,l2) -SymbolSubstIn t))*> & h = <*s1*> ) by A2, FOMODEL0:41, FOMODEL0:34;
then ( h . 1 = s1 & h . 1 = (S -firstChar) . ((l1,l2) -SymbolSubstIn t) ) by FINSEQ_1:40;
then reconsider pp = p as |.(ar ((S -firstChar) . ((l1,l2) -SymbolSubstIn t))).| -element Element of (AllTermsOf S) * ;
(l1,l2) -SymbolSubstIn t = <*((S -firstChar) . ((l1,l2) -SymbolSubstIn t))*> ^ ((S -multiCat) . pp) by A3, A2, FOMODEL0:41;
hence SubTerms ((l1,l2) -SymbolSubstIn t) = (l1 SubstWith l2) * (SubTerms t) by FOMODEL1:def 37; :: thesis: verum

end;

suppose t is 0 -termal ; :: thesis: SubTerms ((l1,l2) -SymbolSubstIn t) = (l1 SubstWith l2) * (SubTerms t)

then reconsider t0 = t as 0 -termal string of S ;
reconsider newt = (l1,l2) -SymbolSubstIn t0 as 0 -termal string of S ;
( SubTerms newt = {} & SubTerms t0 = {} ) ;
hence SubTerms ((l1,l2) -SymbolSubstIn t) = (l1 SubstWith l2) * (SubTerms t) ; :: thesis: verum

end;

end;