let A be non empty set ; :: thesis: for S being CatSignature of A
for a being Element of A holds
( idsym a in the carrier' of S & ( for b being Element of A holds
( homsym (a,b) in the carrier of S & ( for c being Element of A holds compsym (a,b,c) in the carrier' of S ) ) ) )

let S be CatSignature of A; :: thesis: for a being Element of A holds
( idsym a in the carrier' of S & ( for b being Element of A holds
( homsym (a,b) in the carrier of S & ( for c being Element of A holds compsym (a,b,c) in the carrier' of S ) ) ) )

let a be Element of A; :: thesis: ( idsym a in the carrier' of S & ( for b being Element of A holds
( homsym (a,b) in the carrier of S & ( for c being Element of A holds compsym (a,b,c) in the carrier' of S ) ) ) )

A1: the carrier' of () = [:{1},():] \/ [:{2},():] by Def3;
A2: CatSign A is Subsignature of S by Def5;
then A3: the carrier of () c= the carrier of S by INSTALG1:10;
A4: the carrier' of () c= the carrier' of S by ;
<*a*> in 1 -tuples_on A by FINSEQ_2:135;
then [1,<*a*>] in [:{1},():] by ZFMISC_1:105;
then [1,<*a*>] in the carrier' of () by ;
hence idsym a in the carrier' of S by A4; :: thesis: for b being Element of A holds
( homsym (a,b) in the carrier of S & ( for c being Element of A holds compsym (a,b,c) in the carrier' of S ) )

let b be Element of A; :: thesis: ( homsym (a,b) in the carrier of S & ( for c being Element of A holds compsym (a,b,c) in the carrier' of S ) )
A5: the carrier of () = [:,():] by Def3;
<*a,b*> in 2 -tuples_on A by FINSEQ_2:137;
then [0,<*a,b*>] in [:,():] by ZFMISC_1:105;
hence homsym (a,b) in the carrier of S by A3, A5; :: thesis: for c being Element of A holds compsym (a,b,c) in the carrier' of S
let c be Element of A; :: thesis: compsym (a,b,c) in the carrier' of S
<*a,b,c*> in 3 -tuples_on A by FINSEQ_2:139;
then [2,<*a,b,c*>] in [:{2},():] by ZFMISC_1:105;
then [2,<*a,b,c*>] in the carrier' of () by ;
hence compsym (a,b,c) in the carrier' of S by A4; :: thesis: verum