let A be non empty set ; 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; 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; ( 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; 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; ( 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; for c being Element of A holds compsym (a,b,c) in the carrier' of S
let c be Element of A; 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; verum