:: deftheorem Def7 defines delta-concrete CATALG_1:def 7 :
for S being ManySortedSign holds
( S is delta-concrete iff ex f being sequence of NAT st
( ( 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 ) ) & ( 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 ) ) ) );