theorem Th7: :: CATALG_1:7

for S being delta-concrete ManySortedSign
for x being set st ( x in the carrier of S or x in the carrier' of S ) holds
ex i being Element of NAT ex p being FinSequence st
( x = [i,p] & rng p c= underlay S )