theorem Th25: :: NOMIN_1:25

for V, A being set
for m, n being Nat
for S being FinSequence st S IsNDRankSeq V,A & m <= n & n in dom S holds
S . m c= S . n