set S = CatSign A;
( CatSign A is Subsignature of CatSign A & the carrier of (CatSign A) = [:{0},(2 -tuples_on A):] ) by Def3, INSTALG1:15;
then reconsider S = CatSign A as CatSignature by Def4;
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 Def3, INSTALG1:15; :: thesis: verum