reconsider N0 = n --> the Element of X as XFinSequence of X ;
len N0 = n by FUNCOP_1:13;
then N0 is n -element by CARD_1:def 7;
hence ex b₁ being XFinSequence of X st b₁ is n -element ; :: thesis: verum