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

( 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