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