consider k being Element of D such that
A1: k in X by SUBSET_1:4;
reconsider f = n |-> k as FinSequence of X by A1, FINSEQ_2:63;
f is n -element ;
hence ex b₁ being FinSequence of X st b₁ is n -element ; :: thesis: verum