assume the carrier of (CatSign A) = {} ; :: according to INSTALG1:def 1 :: thesis: the carrier' of (CatSign A) = {}
then [:{0},(2 -tuples_on A):] = {} by Def3;
then A = {} ;
then A1: ( 1 <> 0 & 3 <> 0 implies ( 1 -tuples_on A = {} & 3 -tuples_on A = {} ) ) by FINSEQ_3:119;
then [:{1},(1 -tuples_on A):] = {} by ZFMISC_1:90;
then [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] = {} by A1, ZFMISC_1:90;
hence the carrier' of (CatSign A) = {} by Def3; :: thesis: verum