theorem :: FINSEQ_1:96

for i being Nat
for x being object st i > 0 holds
{[i,x]} is FinSubsequence