let s be string of S; ( s = (l1,l2) -SymbolSubstIn phi implies s is 0wff )
assume Z:
s = (l1,l2) -SymbolSubstIn phi
; s is 0wff
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 Lm36;
consider r being relational Element of S, V being abs (ar r) -element Element of (AllTermsOf S) * such that
B0:
phi = <*r*> ^ ((S -multiCat) . V)
by FOMODEL1:def 35;
set m = abs (ar r);
reconsider FV = V as abs (ar r) -element FinSequence of AllTermsOf S by FOMODEL0:26;
reconsider newstrings = f * FV as abs (ar r) -element Element of (AllTermsOf S) * by FINSEQ_1:def 11;
V in TTT *
;
then reconsider VV = V as Element of ((AllSymbolsOf S) *) * ;
Z1:
( 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 23
.=
((l1 SubstWith l2) . <*r*>) ^ ((l1 SubstWith l2) . ((S -multiCat) . VV))
by B0, 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 Z1, RELAT_1:165
;
hence
s is 0wff
by FOMODEL1:def 35, FINSEQ_1:def 11, Z; verum