set k = 1;
consider p being XFinSequence of D such that
A1: len p = 1 by Th12;
p <> {} by A1;
hence not for b₁ being XFinSequence of D holds b₁ is empty ; :: thesis: verum