theorem Th17: :: FIB_NUM2:17

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