theorem :: BALLOT_1:3

for D1, D2 being non empty set
for d1 being XFinSequence of D1
for d2 being XFinSequence of D2 st d1 = d2 holds
XFS2FS d1 = XFS2FS d2 ;