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