for k being Element of NAT
for a being set st k >= 1 holds
{[k,a]} is FinSubsequence