consider d being Element of D;
A1: ( rng <*<*d*>*> = {<*d*>} & <*d*> in D * ) by FINSEQ_1:55, FINSEQ_1:def 11;
then rng <*<*d*>*> c= D * by ZFMISC_1:37;
then reconsider p = <*<*d*>*> as FinSequence of D * by FINSEQ_1:def 4;
reconsider p = p as tabular FinSequence of D * by Th1;
reconsider s = <*d*> as FinSequence ;
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