set Y = Compound (s,Strings);
set SS = AllSymbolsOf S;
reconsider ss = s as Element of AllSymbolsOf S ;

let x be object ; :: thesis:
assume x in Compound (s,Strings) ; :: thesis:
then consider StringTuple being Element of ((AllSymbolsOf S) *) * such that
A1: ( x = <*s*> ^ ((S -multiCat) . StringTuple) & rng StringTuple c= Strings & StringTuple is |.(ar s).| -element ) ;
reconsider head = <*ss*> as non empty FinSequence of AllSymbolsOf S ;
reconsider tail = (S -multiCat) . StringTuple as FinSequence of AllSymbolsOf S by FINSEQ_1:def 11;
( head ^ tail is non empty FinSequence of AllSymbolsOf S & x = head ^ tail ) by A1;
hence x in ((AllSymbolsOf S) *) \ {{}} by FOMODEL0:5; :: thesis:

end;