consider d being Element of D;
A1: rng <*<*d*>*> = {<*d*>} by FINSEQ_1:55;
<*d*> in D * by FINSEQ_1:def 11;
then rng <*<*d*>*> c= D * by A1, ZFMISC_1:37;
then reconsider p = <*<*d*>*> as FinSequence of D * by FINSEQ_1:def 4;
reconsider s = <*d*> as FinSequence ;
reconsider p = p as tabular FinSequence of D * by Th1;
take p ; :: thesis: not p is empty-yielding

now

take s = s; :: thesis: ( s in rng p & s <> {} )
thus s in rng p by A1, TARSKI:def 1; :: thesis: s <> {}
thus s <> {} ; :: thesis: verum

end;

hence not p is empty-yielding by RELAT_1:184; :: thesis: verum