theorem Th17: :: NOMIN_1:17

for V, A being set
for S being FinSequence st S IsNDRankSeq V,A holds
S ^ <*(NDSS (V,(A \/ (S . (len S)))))*> IsNDRankSeq V,A