theorem Th26: :: NOMIN_1:26

for V, A being set
for F being FinSequence st F IsNDRankSeq V,A holds
ex S being FinSequence st
( len S = 1 + (len F) & S IsNDRankSeq V,A & ( for n being Nat st n in dom S holds
S . n = NDSS (V,(A \/ ((<*A*> ^ F) . n))) ) )