let A be set ; 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 Def3;
A2:
for x being object st x in proj2 ( the carrier of (CatSign A) \/ the carrier' of (CatSign A)) holds
x is Function
by Lm2;
hereby TARSKI:def 3,
XBOOLE_0:def 10 A c= underlay (CatSign A)
let x be
object ;
( x in underlay (CatSign A) implies x in A )assume
x in underlay (CatSign A)
;
x in Athen consider a being
set ,
f being
Function such that A3:
[a,f] in the
carrier of
(CatSign A) \/ the
carrier' of
(CatSign A)
and A4:
x in rng f
by Def6, A2;
(
[a,f] in the
carrier of
(CatSign A) or
[a,f] in the
carrier' of
(CatSign A) )
by A3, 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, Def3, 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:87;
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 A4;
verum
end;
let x be object ; TARSKI:def 3 ( not x in A or x in underlay (CatSign A) )
assume
x in A
; x in underlay (CatSign A)
then A5:
<*x,x*> in 2 -tuples_on A
by FINSEQ_2:137;
the carrier of (CatSign A) = [:{0},(2 -tuples_on A):]
by Def3;
then
[0,<*x,x*>] in the carrier of (CatSign A)
by A5, ZFMISC_1:105;
then A6:
[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:127;
then
x in rng <*x,x*>
by TARSKI:def 2;
hence
x in underlay (CatSign A)
by A6, Def6, A2; verum