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