theorem :: AFINSQ_1:64

for D being non empty set
for p being XFinSequence of D st p . 0 = 0 & 0 < len p holds
XFS2FS* p = {}