consider d being Element of D;
A1: {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;

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 ( [x,y1] in {[0 ,d]} & [x,y2] in {[0 ,d]} ) ; :: thesis: y1 = y2
then ( [x,y1] = [0 ,d] & [x,y2] = [0 ,d] ) by TARSKI:def 1;
hence y1 = y2 by ZFMISC_1:33; :: thesis: verum

end;

then reconsider f = {[0 ,d]} as Function by FUNCT_1:def 1, RELAT_1:4;
A2: dom f = 1 by ORDINAL3:18, RELAT_1:23;
then reconsider p = {[0 ,d]} as T-Sequence by ORDINAL1:def 7;
rng p = {d} by RELAT_1:23;
then p is finite T-Sequence of D by A2, A1, AFINSQ_1:7, RELAT_1:def 19;
hence not for b₁ being XFinSequence of D holds b₁ is empty ; :: thesis: verum