consider d being Element of D;
for x, y1, y2 being set st [x,y1] in {[0 ,d]} & [x,y2] in {[0 ,d]} holds
y1 = y2

proof

let x, y1, y2 be set ; :: thesis: ( [x,y1] in {[0 ,d]} & [x,y2] in {[0 ,d]} implies y1 = y2 )
assume A1: ( [x,y1] in {[0 ,d]} & [x,y2] in {[0 ,d]} ) ; :: thesis: y1 = y2
then A2: [x,y1] = [0 ,d] by TARSKI:def 1;
[x,y2] = [0 ,d] by A1, TARSKI:def 1;
hence y1 = y2 by A2, ZFMISC_1:33; :: thesis: verum

end;

then reconsider f = {[0 ,d]} as Function by FUNCT_1:def 1, RELAT_1:4;
A3: dom f = 1 by ORDINAL3:18, RELAT_1:23;
then reconsider p = {[0 ,d]} as T-Sequence by ORDINAL1:def 7;
A4: rng p = {d} by RELAT_1:23;
{d} c= D

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {d} or x in D )
assume x in {d} ; :: thesis: x in D
then x = d by TARSKI:def 1;
hence x in D ; :: thesis: verum

end;

then p is finite T-Sequence of by A3, A4, AFINSQ_1:7, RELAT_1:def 19;
hence not for b₁ being XFinSequence of holds b₁ is empty ; :: thesis: verum