theorem Th30: :: NOMIN_2:31

for V, A being set
for d being TypeSCNominativeData of V,A
for g being b₁,b₂ -FPrg-yielding FinSequence
for X being one-to-one FinSequence st dom g = dom X & d in_doms g holds
rng (NDentry (g,X,d)) c= ND (V,A)