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