set psi = (l1,l2) -SymbolSubstIn phi;
set e = l1 SubstWith l2;
set SS = AllSymbolsOf S;
set TT = AllTermsOf S;
set C = S -multiCat ;
(AllTermsOf S) /\ (((AllSymbolsOf S) *) \ {{}}) =
(AllTermsOf S) null (((AllSymbolsOf S) *) \ {{}})
.=
AllTermsOf S
;
then reconsider TTT = AllTermsOf S as non empty Subset of ((AllSymbolsOf S) *) ;
reconsider f = (l1 SubstWith l2) | (AllTermsOf S) as Function of (AllTermsOf S),(AllTermsOf S) by Lm32;
consider r being relational Element of S, V being |.(ar r).| -element Element of (AllTermsOf S) * such that
A1:
phi = <*r*> ^ ((S -multiCat) . V)
by FOMODEL1:def 35;
set m = |.(ar r).|;
reconsider FV = V as |.(ar r).| -element FinSequence of AllTermsOf S by FOMODEL0:26;
reconsider newstrings = f * FV as |.(ar r).| -element FinSequence of AllTermsOf S ;
V in TTT *
;
then reconsider VV = V as Element of ((AllSymbolsOf S) *) * ;
A2:
( rng V c= AllTermsOf S & dom f = AllTermsOf S )
by FUNCT_2:def 1, RELAT_1:def 19;
(l1,l2) -SymbolSubstIn phi =
(l1 SubstWith l2) . phi
by FOMODEL0:def 22
.=
((l1 SubstWith l2) . <*r*>) ^ ((l1 SubstWith l2) . ((S -multiCat) . VV))
by A1, FOMODEL0:36
.=
<*r*> ^ ((l1 SubstWith l2) . ((S -multiCat) . VV))
by FOMODEL0:35
.=
<*r*> ^ ((S -multiCat) . ((l1 SubstWith l2) * VV))
by FOMODEL0:37
.=
<*r*> ^ ((S -multiCat) . newstrings)
by A2, RELAT_1:165
;
hence
for b1 being string of S st b1 = (l1,l2) -SymbolSubstIn phi holds
b1 is 0wff
; verum