n --> 0 is n -element ;
hence ex b₁ being XFinSequence st b₁ is n -element ; :: thesis: verum