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

proof

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

per cases ;

suppose A2: i = 0 ; :: thesis:

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

end;

suppose A3: i = 1 ; :: thesis:

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

end;

suppose A4: i = 2 ; :: thesis:

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

end;

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

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

end;

consider f being Function such that
A6: ( dom f = NAT & rng f c= NAT ) and
A7: for i being set st i in NAT holds
S₁[i,f . i] from WELLORD2:sch 1(A1);
reconsider f = f as Function of NAT ,NAT by A6, FUNCT_2:4;
A8: the carrier of (CatSign A) = [:{0 },(2 -tuples_on A):] by Def5;
A9: the carrier' of (CatSign A) = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] by Def5;
A10: A = underlay (CatSign A) by Th15;
take f ; :: according to CATALG_1:def 9 :: thesis:

hereby :: thesis:

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

end;

let o be set ; :: thesis:
assume A12: o in the carrier' of (CatSign A) ; :: thesis:

per cases by A9, A12, XBOOLE_0:def 3;

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

then consider i, p being set such that
A13: ( i in {1} & p in 1 -tuples_on A & o = [i,p] ) by ZFMISC_1:103;
reconsider p = p as FinSequence of A by A13, 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 A9, A10, A13, Th4, TARSKI:def 1, XBOOLE_1:7; :: thesis:

end;

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

then consider i, p being set such that
A14: ( i in {2} & p in 3 -tuples_on A & o = [i,p] ) by ZFMISC_1:103;
reconsider p = p as FinSequence of A by A14, 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 A9, A10, A14, Th4, TARSKI:def 1, XBOOLE_1:7; :: thesis:

end;