defpred S₁[ object , object ] means ( ( A = 0 implies c₂ = 2 ) & ( A = 1 implies c₂ = 1 ) & ( A = 2 implies c₂ = 3 ) );
set S = CatSign A;
A1: for x being object st x in NAT holds
ex y being object st
( y in NAT & S₁[x,y] )

reconsider j0 = 2, j1 = 1, j2 = 3 as set ;
let i be object ; :: thesis:
assume i in NAT ; :: thesis:

suppose A2: i = 0 ; :: thesis:

take j0 ; :: thesis:
thus ( j0 in NAT & S₁[i,j0] ) by A2; :: thesis:

end;

suppose A3: i = 1 ; :: thesis:

take j1 ; :: thesis:
thus ( j1 in NAT & S₁[i,j1] ) by A3; :: thesis:

end;

suppose A4: i = 2 ; :: thesis:

take j2 ; :: thesis:
thus ( j2 in NAT & S₁[i,j2] ) by A4; :: thesis:

end;

suppose A5: ( i <> 0 & i <> 1 & i <> 2 ) ; :: thesis:

take j0 ; :: thesis:
thus ( j0 in NAT & S₁[i,j0] ) by A5; :: thesis:

end;

end;

end;

consider f being Function such that
A6: ( dom f = NAT & rng f c= NAT ) and
A7: for i being object st i in NAT holds
S₁[i,f . i] from FUNCT_1:sch 6(A1);
reconsider f = f as sequence of NAT by A6, FUNCT_2:2;
take f ; :: according to CATALG_1:def 7 :: thesis:
A8: A = underlay (CatSign A) by Th5;
A9: the carrier of (CatSign A) = [:{0},(2 -tuples_on A):] by Def3;

hereby :: thesis:

let s be object ; :: thesis:
assume s in the carrier of (CatSign A) ; :: thesis:
then consider i, p being object such that
A10: i in {0} and
A11: p in 2 -tuples_on A and
A12: s = [i,p] by A9, ZFMISC_1:84;
reconsider p = p as FinSequence by A11;
take i = 0 ; :: thesis:
take p = p; :: thesis:
f . i = 2 by A7;
hence ( s = [i,p] & len p = f . i ) by A10, A11, A12, FINSEQ_2:132, TARSKI:def 1; :: thesis:
thus [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier of (CatSign A) by A7, A9, A8; :: thesis:

end;

let o be object ; :: thesis:
A13: the carrier' of (CatSign A) = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] by Def3;
assume A14: o in the carrier' of (CatSign A) ; :: thesis:

per cases by A13, A14, XBOOLE_0:def 3;

suppose o in [:{1},(1 -tuples_on A):] ; :: thesis:

then consider i, p being object such that
A15: i in {1} and
A16: p in 1 -tuples_on A and
A17: o = [i,p] by ZFMISC_1:84;
reconsider p = p as FinSequence of A by A16, FINSEQ_2:def 3;
take i = 1; :: thesis:
take p ; :: thesis:
f . i = 1 by A7;
hence ( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier' of (CatSign A) ) by A13, A8, A15, A16, A17, FINSEQ_2:132, TARSKI:def 1, XBOOLE_1:7; :: thesis:

end;

suppose o in [:{2},(3 -tuples_on A):] ; :: thesis:

then consider i, p being object such that
A18: i in {2} and
A19: p in 3 -tuples_on A and
A20: o = [i,p] by ZFMISC_1:84;
reconsider p = p as FinSequence of A by A19, FINSEQ_2:def 3;
take i = 2; :: thesis:
take p ; :: thesis:
f . i = 3 by A7;
hence ( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier' of (CatSign A) ) by A13, A8, A18, A19, A20, FINSEQ_2:132, TARSKI:def 1, XBOOLE_1:7; :: thesis:

end;

end;