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