let S be non empty Categorial delta-concrete Signature; S is CatSignature of underlay S
consider s being SortSymbol of S;
consider A being set such that
A1:
CatSign A is Subsignature of S
and
A2:
the carrier of S = [:{0},(2 -tuples_on A):]
by Def6;
consider f being Function of NAT,NAT such that
A3:
for s being set st s in the carrier of S 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 S)):] c= the carrier of S )
and
for o being set st o in the carrier' of S 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 S)):] c= the carrier' of S )
by Def9;
consider i being Element of NAT , p being FinSequence such that
A4:
s = [i,p]
and
A5:
( len p = f . i & [:{i},((f . i) -tuples_on (underlay S)):] c= the carrier of S )
by A3;
p in 2 -tuples_on A
by A2, A4, ZFMISC_1:128;
then A6:
len p = 2
by FINSEQ_2:152;
A7:
A c= underlay S
proof
let x be
set ;
TARSKI:def 3 ( not x in A or x in underlay S )
assume
x in A
;
x in underlay S
then
<*x,x*> in 2
-tuples_on A
by FINSEQ_2:157;
then
[0,<*x,x*>] in the
carrier of
S
by A2, ZFMISC_1:128;
then A8:
[0,<*x,x*>] in the
carrier of
S \/ the
carrier' of
S
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 S
by A8, Def8;
verum
end;
i = 0
by A2, A4, ZFMISC_1:128;
then A9:
2 -tuples_on (underlay S) c= 2 -tuples_on A
by A2, A5, A6, ZFMISC_1:117;
underlay S c= A
then
A = underlay S
by A7, XBOOLE_0:def 10;
hence
S is CatSignature of underlay S
by A1, A2, Def7; verum