rng {} c= D ;
hence ex b₁ being FinSequence st rng b₁ c= D ; :: thesis: verum