theorem :: FINSEQ_3:157

for x being object
for i being Nat
for q being FinSubsequence st q = {[i,x]} holds
Seq q = <*x*>