rng (0 |-> 0) c= D by XBOOLE_1:2;
then ( 0 |-> 0 is empty-yielding & 0 |-> 0 is D -valued ) by FINSEQ_1:def 4;
hence ex b₁ being D -valued FinSequence st b₁ is empty-yielding ; :: thesis: verum