set TS = TermSymbolsOf S;
set AS = AtomicFormulaSymbolsOf S;
set F = S -firstChar ;
set C = S -multiCat ;
set TT = AllTermsOf S;
set CC = (TermSymbolsOf S) -multiCat ;
set SS = AllSymbolsOf S;
let w be string of S; :: thesis: ( w is 0wff implies w is AtomicFormulaSymbolsOf S -valued )
assume w is 0wff ; :: thesis: w is AtomicFormulaSymbolsOf S -valued
then reconsider phi = w as 0wff string of S ;
reconsider r = (S -firstChar) . phi as relational Element of S ;
set m = |.(ar r).|;
reconsider rr = r as Element of AtomicFormulaSymbolsOf S by Def20;
reconsider sub = SubTerms phi as |.(ar r).| + 0 -element Element of (AllTermsOf S) * ;
(AllTermsOf S) \ ((TermSymbolsOf S) *) = {} ;
then ( TermSymbolsOf S c= AllSymbolsOf S & AllTermsOf S c= (TermSymbolsOf S) * & sub is AllTermsOf S -valued ) by XBOOLE_1:1, XBOOLE_1:37;
then <*rr*> ^ (((TermSymbolsOf S) -multiCat) . sub) = <*r*> ^ ((S -multiCat) . sub) by FOMODEL0:53
.= phi by Def38 ;
hence w is AtomicFormulaSymbolsOf S -valued ; :: thesis: verum