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

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