theorem :: FINSEQ_3:159

for x being object
for q being FinSubsequence st Seq q = <*x*> holds
ex i being Element of NAT st q = {[i,x]}