let S be CatSignature of A; :: thesis: S is Categorial
take A ; :: according to CATALG_1:def 4 :: 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 Def5; :: thesis: verum