take Union (FNDSC (V,A)) ; :: thesis: for b₁ being Function st ex S being FinSequence st
( S IsNDRankSeq V,A & b₁ in Union S ) holds
b₁ in Union (FNDSC (V,A))
thus for b₁ being Function st ex S being FinSequence st
( S IsNDRankSeq V,A & b₁ in Union S ) holds
b₁ in Union (FNDSC (V,A)) by Lm1; :: thesis: verum