let S be Language; 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; 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; 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
;
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;
verum end;