theorem Th4: :: BALLOT_1:4

for D being non empty set
for d1, d2 being XFinSequence of D st XFS2FS d1 = XFS2FS d2 holds
d1 = d2