defpred S_{1}[ object , object ] means ( ( A = 0 implies c_{2} = 2 ) & ( A = 1 implies c_{2} = 1 ) & ( A = 2 implies c_{2} = 3 ) );

set S = CatSign A;

A1: for x being object st x in NAT holds

ex y being object st

( y in NAT & S_{1}[x,y] )

A6: ( dom f = NAT & rng f c= NAT ) and

A7: for i being object st i in NAT holds

S_{1}[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: ( ( for s being object st s in the carrier of (CatSign A) 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 (CatSign A))):] c= the carrier of (CatSign A) ) ) & ( for o being object st o in the carrier' of (CatSign A) 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 (CatSign A))):] c= the carrier' of (CatSign A) ) ) )

A8: A = underlay (CatSign A) by Th5;

A9: the carrier of (CatSign A) = [:{0},(2 -tuples_on A):] by Def3;

( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier' of (CatSign A) ) )

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: ex i being Element of NAT ex p being FinSequence st

( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier' of (CatSign A) )

set S = CatSign A;

A1: for x being object st x in NAT holds

ex y being object st

( y in NAT & S

proof

consider f being Function such that
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 & S_{1}[i,y] ) )

assume i in NAT ; :: thesis: ex y being object st

( y in NAT & S_{1}[i,y] )

end;let i be object ; :: thesis: ( i in NAT implies ex y being object st

( y in NAT & S

assume i in NAT ; :: thesis: ex y being object st

( y in NAT & S

per cases
( i = 0 or i = 1 or i = 2 or ( i <> 0 & i <> 1 & i <> 2 ) )
;

end;

suppose A2:
i = 0
; :: thesis: ex y being object st

( y in NAT & S_{1}[i,y] )

( y in NAT & S

take
j0
; :: thesis: ( j0 in NAT & S_{1}[i,j0] )

thus ( j0 in NAT & S_{1}[i,j0] )
by A2; :: thesis: verum

end;thus ( j0 in NAT & S

suppose A3:
i = 1
; :: thesis: ex y being object st

( y in NAT & S_{1}[i,y] )

( y in NAT & S

take
j1
; :: thesis: ( j1 in NAT & S_{1}[i,j1] )

thus ( j1 in NAT & S_{1}[i,j1] )
by A3; :: thesis: verum

end;thus ( j1 in NAT & S

suppose A4:
i = 2
; :: thesis: ex y being object st

( y in NAT & S_{1}[i,y] )

( y in NAT & S

take
j2
; :: thesis: ( j2 in NAT & S_{1}[i,j2] )

thus ( j2 in NAT & S_{1}[i,j2] )
by A4; :: thesis: verum

end;thus ( j2 in NAT & S

A6: ( dom f = NAT & rng f c= NAT ) and

A7: for i being object st i in NAT holds

S

reconsider f = f as sequence of NAT by A6, FUNCT_2:2;

take f ; :: according to CATALG_1:def 7 :: thesis: ( ( for s being object st s in the carrier of (CatSign A) 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 (CatSign A))):] c= the carrier of (CatSign A) ) ) & ( for o being object st o in the carrier' of (CatSign A) 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 (CatSign A))):] c= the carrier' of (CatSign A) ) ) )

A8: A = underlay (CatSign A) by Th5;

A9: the carrier of (CatSign A) = [:{0},(2 -tuples_on A):] by Def3;

hereby :: thesis: for o being object st o in the carrier' of (CatSign A) 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 (CatSign A))):] c= the carrier' of (CatSign A) )

let o be object ; :: thesis: ( o in the carrier' of (CatSign A) implies ex i being Element of NAT ex p being FinSequence st ex i being Element of NAT ex p being FinSequence st

( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier' of (CatSign A) )

let s be object ; :: thesis: ( s in the carrier of (CatSign A) 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 (CatSign A))):] c= the carrier of (CatSign A) ) )

assume s in the carrier of (CatSign A) ; :: 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 (CatSign A))):] c= the carrier of (CatSign A) )

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: ex p being FinSequence st

( s = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier of (CatSign A) )

take p = p; :: thesis: ( s = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier of (CatSign A) )

f . i = 2 by A7;

hence ( s = [i,p] & len p = f . i ) by A10, A11, A12, FINSEQ_2:132, TARSKI:def 1; :: thesis: [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier of (CatSign A)

thus [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier of (CatSign A) by A7, A9, A8; :: thesis: verum

end;( s = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier of (CatSign A) ) )

assume s in the carrier of (CatSign A) ; :: 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 (CatSign A))):] c= the carrier of (CatSign A) )

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: ex p being FinSequence st

( s = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier of (CatSign A) )

take p = p; :: thesis: ( s = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier of (CatSign A) )

f . i = 2 by A7;

hence ( s = [i,p] & len p = f . i ) by A10, A11, A12, FINSEQ_2:132, TARSKI:def 1; :: thesis: [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier of (CatSign A)

thus [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier of (CatSign A) by A7, A9, A8; :: thesis: verum

( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier' of (CatSign A) ) )

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: ex i being Element of NAT ex p being FinSequence st

( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier' of (CatSign A) )

per cases
( o in [:{1},(1 -tuples_on A):] or o in [:{2},(3 -tuples_on A):] )
by A13, A14, XBOOLE_0:def 3;

end;

suppose
o in [:{1},(1 -tuples_on A):]
; :: 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 (CatSign A))):] c= the carrier' of (CatSign A) )

( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier' of (CatSign A) )

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: ex p being FinSequence st

( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier' of (CatSign A) )

take p ; :: thesis: ( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier' of (CatSign A) )

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: verum

end;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: ex p being FinSequence st

( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier' of (CatSign A) )

take p ; :: thesis: ( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier' of (CatSign A) )

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: verum

suppose
o in [:{2},(3 -tuples_on A):]
; :: 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 (CatSign A))):] c= the carrier' of (CatSign A) )

( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier' of (CatSign A) )

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: ex p being FinSequence st

( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier' of (CatSign A) )

take p ; :: thesis: ( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier' of (CatSign A) )

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: verum

end;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: ex p being FinSequence st

( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier' of (CatSign A) )

take p ; :: thesis: ( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier' of (CatSign A) )

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: verum