let S be Language; for l1, l2 being literal Element of S
for phi0 being 0wff string of S holds SubTerms ((l1,l2) -SymbolSubstIn phi0) = (l1 SubstWith l2) * (SubTerms phi0)
let l1, l2 be literal Element of S; for phi0 being 0wff string of S holds SubTerms ((l1,l2) -SymbolSubstIn phi0) = (l1 SubstWith l2) * (SubTerms phi0)
let phi0 be 0wff string of S; SubTerms ((l1,l2) -SymbolSubstIn phi0) = (l1 SubstWith l2) * (SubTerms phi0)
set s = l1 SubstWith l2;
set psi0 = (l1,l2) -SymbolSubstIn phi0;
set ST1 = SubTerms phi0;
set F = S -firstChar ;
set C = S -multiCat ;
set ST2 = SubTerms ((l1,l2) -SymbolSubstIn phi0);
set SS = AllSymbolsOf S;
set TT = AllTermsOf S;
reconsider TTT = AllTermsOf S as Subset of ((AllSymbolsOf S) *) by XBOOLE_1:1;
A1:
( rng (SubTerms phi0) 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;
reconsider r1 = (S -firstChar) . phi0, r2 = (S -firstChar) . ((l1,l2) -SymbolSubstIn phi0) as relational Element of S ;
phi0 . 1 = r1
by FOMODEL0:6;
then
( r1 = phi0 . 1 & ((l1,l2) -SymbolSubstIn phi0) . 1 = phi0 . 1 )
by FUNCT_4:105;
then A2:
r1 = r2
by FOMODEL0:6;
set n1 = |.(ar r1).|;
set n2 = |.(ar r2).|;
(l1 SubstWith l2) * (SubTerms phi0) = ss * (SubTerms phi0)
by RELAT_1:165, A1;
then
(l1 SubstWith l2) * (SubTerms phi0) is |.(ar r2).| -element FinSequence of AllTermsOf S
by FOMODEL0:26, A2;
then reconsider ST22 = (l1 SubstWith l2) * (SubTerms phi0) as |.(ar r2).| -element Element of (AllTermsOf S) * ;
reconsider ST11 = SubTerms phi0 as (AllSymbolsOf S) * -valued FinSequence ;
phi0 = <*r1*> ^ ((S -multiCat) . (SubTerms phi0))
by FOMODEL1:def 38;
then (l1 SubstWith l2) . phi0 =
((l1 SubstWith l2) . <*r1*>) ^ ((l1 SubstWith l2) . ((S -multiCat) . (SubTerms phi0)))
by FOMODEL0:36
.=
<*r1*> ^ ((l1 SubstWith l2) . ((S -multiCat) . (SubTerms phi0)))
by FOMODEL0:35
.=
<*r2*> ^ ((S -multiCat) . ST22)
by FOMODEL0:37, A2
;
then
(l1,l2) -SymbolSubstIn phi0 = <*r2*> ^ ((S -multiCat) . ST22)
by FOMODEL0:def 22;
hence
SubTerms ((l1,l2) -SymbolSubstIn phi0) = (l1 SubstWith l2) * (SubTerms phi0)
by FOMODEL1:def 38; verum