consider X being non empty set such that
A1: X in D by SETFAM_1:def 10;
A2: rng <*<*X*>*> = {<*X*>} by FINSEQ_1:39;
<*X*> in D * by A1, FUNCT_7:18;
then rng <*<*X*>*> c= D * by A2, ZFMISC_1:31;
then reconsider F = <*<*X*>*> as FinSequence of D * by FINSEQ_1:def 4;
take F ; :: thesis: ( not F is empty & F is non-empty )
thus not F is empty ; :: thesis: F is non-empty
assume {} in rng F ; :: according to RELAT_1:def 9 :: thesis: contradiction
hence contradiction by A2; :: thesis: verum