set SS = AllSymbolsOf S;
set C = S -multiCat ;
reconsider header = <*s*> as Element of (AllSymbolsOf S) * ;
reconsider tailer = (S -multiCat) . V as FinSequence of AllSymbolsOf S by FINSEQ_1:def 11;
reconsider IT = header ^ tailer as FinSequence of AllSymbolsOf S ;
( IT in (AllSymbolsOf S) * & not IT in {{}} ) ;
hence <*s*> ^ ((S -multiCat) . V) is string of S by XBOOLE_0:def 5; :: thesis: verum