let S be non empty Signature; :: thesis: ( S is Categorial implies not S is void )
given A being set such that A1: ( CatSign A is Subsignature of S & the carrier of S = [:{0 },(2 -tuples_on A):] ) ; :: according to CATALG_1:def 6 :: thesis: not S is void
consider s being SortSymbol of S;
consider z, p being set such that
A2: ( z in {0 } & p in 2 -tuples_on A & s = [z,p] ) by A1, ZFMISC_1:103;
2 -tuples_on A = { q where q is Element of A * : len q = 2 } by FINSEQ_2:def 4;
then consider q being Element of A * such that
A3: ( p = q & len q = 2 ) by A2;
dom q = Seg 2 by A3, FINSEQ_1:def 3;
then 1 in dom q by FINSEQ_1:4, TARSKI:def 2;
then A4: ( q . 1 in rng q & rng q c= A ) by FUNCT_1:def 5;
then reconsider A' = A as non empty set ;
reconsider a = q . 1 as Element of A' by A4;
<*a*> is Element of 1 -tuples_on A' by FINSEQ_2:118;
then ( [1,<*a*>] in [:{1},(1 -tuples_on A):] & the carrier' of (CatSign A) = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] ) by Def5, ZFMISC_1:128;
then ( [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] c= the carrier' of S & [1,<*a*>] in [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] ) by A1, INSTALG1:11, XBOOLE_0:def 3;
hence not the carrier' of S is empty ; :: according to STRUCT_0:def 13 :: thesis: verum