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 (CatSign A) = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] by Def3;
A2: CatSign A is Subsignature of S by Def5;
then A3: the carrier of (CatSign A) c= the carrier of S by INSTALG1:10;
A4: the carrier' of (CatSign A) c= the carrier' of S by A2, INSTALG1:10;
<*a*> in 1 -tuples_on A by FINSEQ_2:135;
then [1,<*a*>] in [:{1},(1 -tuples_on A):] by ZFMISC_1:105;
then [1,<*a*>] in the carrier' of (CatSign A) by A1, XBOOLE_0:def 3;
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 (CatSign A) = [:{0},(2 -tuples_on A):] by Def3;
<*a,b*> in 2 -tuples_on A by FINSEQ_2:137;
then [0,<*a,b*>] in [:{0},(2 -tuples_on A):] 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},(3 -tuples_on A):] by ZFMISC_1:105;
then [2,<*a,b,c*>] in the carrier' of (CatSign A) by A1, XBOOLE_0:def 3;
hence compsym (a,b,c) in the carrier' of S by A4; :: thesis: verum