theorem Th19: :: NOMIN_1:19

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 = (FNDSC (V,A)) . n