defpred S1[ object , object ] means ( ( A = 0 implies c2 = 2 ) & ( A = 1 implies c2 = 1 ) & ( A = 2 implies c2 = 3 ) );
set S = CatSign A;
A1: for x being object st x in NAT holds
ex y being object st
( y in NAT & S1[x,y] )
proof
reconsider j0 = 2, j1 = 1, j2 = 3 as set ;
let i be object ; :: thesis: ( i in NAT implies ex y being object st
( y in NAT & S1[i,y] ) )

assume i in NAT ; :: thesis: ex y being object st
( y in NAT & S1[i,y] )

per cases ( i = 0 or i = 1 or i = 2 or ( i <> 0 & i <> 1 & i <> 2 ) ) ;
suppose A2: i = 0 ; :: thesis: ex y being object st
( y in NAT & S1[i,y] )

take j0 ; :: thesis: ( j0 in NAT & S1[i,j0] )
thus ( j0 in NAT & S1[i,j0] ) by A2; :: thesis: verum
end;
suppose A3: i = 1 ; :: thesis: ex y being object st
( y in NAT & S1[i,y] )

take j1 ; :: thesis: ( j1 in NAT & S1[i,j1] )
thus ( j1 in NAT & S1[i,j1] ) by A3; :: thesis: verum
end;
suppose A4: i = 2 ; :: thesis: ex y being object st
( y in NAT & S1[i,y] )

take j2 ; :: thesis: ( j2 in NAT & S1[i,j2] )
thus ( j2 in NAT & S1[i,j2] ) by A4; :: thesis: verum
end;
suppose A5: ( i <> 0 & i <> 1 & i <> 2 ) ; :: thesis: ex y being object st
( y in NAT & S1[i,y] )

take j0 ; :: thesis: ( j0 in NAT & S1[i,j0] )
thus ( j0 in NAT & S1[i,j0] ) by A5; :: thesis: verum
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
S1[i,f . i] from reconsider f = f as sequence of NAT by ;
take f ; :: according to CATALG_1:def 7 :: thesis: ( ( for s being object st s in the carrier of () holds
ex i being Element of NAT ex p being FinSequence st
( s = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay ())):] c= the carrier of () ) ) & ( for o being object st o in the carrier' of () holds
ex i being Element of NAT ex p being FinSequence st
( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay ())):] c= the carrier' of () ) ) )

A8: A = underlay () by Th5;
A9: the carrier of () = [:,():] by Def3;
hereby :: thesis: for o being object st o in the carrier' of () holds
ex i being Element of NAT ex p being FinSequence st
( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay ())):] c= the carrier' of () )
let s be object ; :: thesis: ( s in the carrier of () implies ex i being Element of NAT ex p being FinSequence st
( s = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay ())):] c= the carrier of () ) )

assume s in the carrier of () ; :: thesis: ex i being Element of NAT ex p being FinSequence st
( s = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay ())):] c= the carrier of () )

then consider i, p being object such that
A10: i in and
A11: p in 2 -tuples_on A and
A12: s = [i,p] by ;
reconsider p = p as FinSequence by A11;
take i = 0 ; :: thesis: ex p being FinSequence st
( s = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay ())):] c= the carrier of () )

take p = p; :: thesis: ( s = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay ())):] c= the carrier of () )
f . i = 2 by A7;
hence ( s = [i,p] & len p = f . i ) by ; :: thesis: [:{i},((f . i) -tuples_on (underlay ())):] c= the carrier of ()
thus [:{i},((f . i) -tuples_on (underlay ())):] c= the carrier of () by A7, A9, A8; :: thesis: verum
end;
let o be object ; :: thesis: ( o in the carrier' of () implies ex i being Element of NAT ex p being FinSequence st
( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay ())):] c= the carrier' of () ) )

A13: the carrier' of () = [:{1},():] \/ [:{2},():] by Def3;
assume A14: o in the carrier' of () ; :: thesis: ex i being Element of NAT ex p being FinSequence st
( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay ())):] c= the carrier' of () )

per cases ( o in [:{1},():] or o in [:{2},():] ) by ;
suppose o in [:{1},():] ; :: thesis: ex i being Element of NAT ex p being FinSequence st
( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay ())):] c= the carrier' of () )

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 ;
take i = 1; :: thesis: ex p being FinSequence st
( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay ())):] c= the carrier' of () )

take p ; :: thesis: ( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay ())):] c= the carrier' of () )
f . i = 1 by A7;
hence ( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay ())):] c= the carrier' of () ) by ; :: thesis: verum
end;
suppose o in [:{2},():] ; :: thesis: ex i being Element of NAT ex p being FinSequence st
( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay ())):] c= the carrier' of () )

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 ;
take i = 2; :: thesis: ex p being FinSequence st
( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay ())):] c= the carrier' of () )

take p ; :: thesis: ( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay ())):] c= the carrier' of () )
f . i = 3 by A7;
hence ( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay ())):] c= the carrier' of () ) by ; :: thesis: verum
end;
end;