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

now :: thesis: ex s being FinSequence st
( s in rng p & s <> {} )

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:149; :: thesis: verum