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;
hence CatSign A is strict CatSignature of A by Def5; :: thesis: verum