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 Def5;
A2: CatSign A is Subsignature of S by Def7;
then A3: the carrier of (CatSign A) c= the carrier of S by INSTALG1:11;
A4: the carrier' of (CatSign A) c= the carrier' of S by A2, INSTALG1:11;
<*a*> in 1 -tuples_on A by FINSEQ_2:155;
then [1,<*a*>] in [:{1},(1 -tuples_on A):] by ZFMISC_1:128;
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 Def5;
<*a,b*> in 2 -tuples_on A by FINSEQ_2:157;
then [0 ,<*a,b*>] in [:{0 },(2 -tuples_on A):] by ZFMISC_1:128;
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:159;
then [2,<*a,b,c*>] in [:{2},(3 -tuples_on A):] by ZFMISC_1:128;
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