set S = CatSign A;
( CatSign A is Subsignature of CatSign A & the carrier of (CatSign A) = [:{0 },(2 -tuples_on A):] ) by Def5, INSTALG1:16;
then reconsider S = CatSign A as CatSignature by Def6;
take S ; :: thesis: ( CatSign A is Subsignature of S & the carrier of S = [:{0 },(2 -tuples_on A):] )
thus ( CatSign A is Subsignature of S & the carrier of S = [:{0 },(2 -tuples_on A):] ) by Def5, INSTALG1:16; :: thesis: verum