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

now :: thesis: for x being object st x in Compound (s,Strings) holds
x in ((AllSymbolsOf S) *) \ {{}}

let x be object ; :: thesis: ( x in Compound (s,Strings) implies x in ((AllSymbolsOf S) *) \ {{}} )
assume x in Compound (s,Strings) ; :: thesis: x in ((AllSymbolsOf S) *) \ {{}}
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: verum

end;

hence Compound (s,Strings) is Element of bool (((AllSymbolsOf S) *) \ {{}}) by TARSKI:def 3; :: thesis: verum