for O being non empty connected Poset
for R being array of O
for C being 0 -based arr_computation of R st R is finite array of O holds
C is finite