theorem :: CATALG_1:9

for S being delta-concrete ManySortedSign
for i being set
for p1, p2 being FinSequence st len p2 = len p1 & rng p2 c= underlay S holds
( ( [i,p1] in the carrier of S implies [i,p2] in the carrier of S ) & ( [i,p1] in the carrier' of S implies [i,p2] in the carrier' of S ) )