set SS = AllSymbolsOf S;
set s = the relational Element of S;
set V = the |.(ar the relational Element of S).| -element Element of (AllTermsOf S) * ;
reconsider ss = the relational Element of S as Element of AllSymbolsOf S ;
reconsider tail = (S -multiCat) . the |.(ar the relational Element of S).| -element Element of (AllTermsOf S) * as FinSequence of AllSymbolsOf S by FINSEQ_1:def 11;
reconsider IT = <*ss*> ^ tail as Element of ((AllSymbolsOf S) *) \ {{}} by FOMODEL0:5;
take IT ; :: thesis: IT is 0wff
thus IT is 0wff ; :: thesis: verum