theorem Th16: :: NOMIN_1:16

for V, A being set
for n being Nat
for S being FinSequence st S IsNDRankSeq V,A & n in dom S holds
S | n IsNDRankSeq V,A