let S be non empty Signature; ( S is Categorial implies not S is void )
given A being set such that A1:
CatSign A is Subsignature of S
and
A2:
the carrier of S = [:{0},(2 -tuples_on A):]
; CATALG_1:def 4 not S is void
set s = the SortSymbol of S;
consider z, p being object such that
z in {0}
and
A3:
p in 2 -tuples_on A
and
the SortSymbol of S = [z,p]
by A2, ZFMISC_1:84;
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
p = q
and
A4:
len q = 2
by A3;
A5:
dom q = Seg 2
by A4, FINSEQ_1:def 3;
then reconsider A9 = A as non empty set ;
1 in dom q
by A5, FINSEQ_1:2, TARSKI:def 2;
then
q . 1 in rng q
by FUNCT_1:def 3;
then reconsider a = q . 1 as Element of A9 ;
the carrier' of (CatSign A) = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):]
by Def3;
then
( <*a*> is Element of 1 -tuples_on A9 & [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] c= the carrier' of S )
by A1, FINSEQ_2:98, INSTALG1:10;
hence
not the carrier' of S is empty
; STRUCT_0:def 13 verum