Union <*(NDSS (V,A))*> = NDSS (V,A) by FINSEQ_3:135;
then the PartFunc of V,A | {} in Union <*(NDSS (V,A))*> ;
hence ex b₁ being Function ex S being FinSequence st
( S IsNDRankSeq V,A & b₁ in Union S ) by Th27; :: thesis: verum