card (n --> 0) = n ;
then n --> 0 is n -element by CARD_1:def 7;
hence ex b₁ being natural-valued XFinSequence st b₁ is n -element ; :: thesis: verum