for O being non empty connected Poset
for R being array of O
for C being finite arr_computation of R holds
( last C is permutation of R & ( for a being Ordinal st a in dom C holds
C . a is permutation of R ) )