rng {} c= D ;
hence {} is FinSequence of D by Def4; :: thesis: verum