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