let S be non empty Categorial delta-concrete Signature; S is CatSignature of underlay S
set s = the 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 Def4;
consider f being sequence of NAT such that
A3:
for s being object 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 object 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 Def7;
consider i being Element of NAT , p being FinSequence such that
A4:
the SortSymbol of 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:105;
then A6:
len p = 2
by FINSEQ_2:132;
A7:
for x being object st x in proj2 ( the carrier of S \/ the carrier' of S) holds
x is Function
by Lm3;
A8:
A c= underlay S
proof
let x be
object ;
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:137;
then
[0,<*x,x*>] in the
carrier of
S
by A2, ZFMISC_1:105;
then A9:
[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:127;
then
x in rng <*x,x*>
by TARSKI:def 2;
hence
x in underlay S
by A9, Def6, A7;
verum
end;
i = 0
by A2, A4, ZFMISC_1:105;
then A10:
2 -tuples_on (underlay S) c= 2 -tuples_on A
by A2, A5, A6, ZFMISC_1:94;
underlay S c= A
then
A = underlay S
by A8;
hence
S is CatSignature of underlay S
by A1, A2, Def5; verum