let A be set ; :: thesis: underlay (CatSign A) = A
set S = CatSign A;
A1: the carrier' of (CatSign A) = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] by Def5;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: A c= underlay (CatSign A)

let x be set ; :: thesis: ( x in underlay (CatSign A) implies x in A )
assume x in underlay (CatSign A) ; :: thesis: x in A
then consider a being set , f being Function such that
A2: [a,f] in the carrier of (CatSign A) \/ the carrier' of (CatSign A) and
A3: x in rng f by Def8;
( [a,f] in the carrier of (CatSign A) or [a,f] in the carrier' of (CatSign A) ) by A2, XBOOLE_0:def 3;
then ( [a,f] in [:{0},(2 -tuples_on A):] or [a,f] in [:{1},(1 -tuples_on A):] or [a,f] in [:{2},(3 -tuples_on A):] ) by A1, Def5, XBOOLE_0:def 3;
then ( f in 2 -tuples_on A or f in 1 -tuples_on A or f in 3 -tuples_on A ) by ZFMISC_1:106;
then f is FinSequence of A by FINSEQ_2:def 3;
then rng f c= A by FINSEQ_1:def 4;
hence x in A by A3; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in underlay (CatSign A) )
assume x in A ; :: thesis: x in underlay (CatSign A)
then A4: <*x,x*> in 2 -tuples_on A by FINSEQ_2:157;
the carrier of (CatSign A) = [:{0},(2 -tuples_on A):] by Def5;
then [0,<*x,x*>] in the carrier of (CatSign A) by A4, ZFMISC_1:128;
then A5: [0,<*x,x*>] in the carrier of (CatSign A) \/ the carrier' of (CatSign A) by XBOOLE_0:def 3;
rng <*x,x*> = {x,x} by FINSEQ_2:147;
then x in rng <*x,x*> by TARSKI:def 2;
hence x in underlay (CatSign A) by A5, Def8; :: thesis: verum