for D being set
for F being FinSequence of D *
for k being set st k in dom (FlattenSeq F) holds
ex i, j being Nat st
( i in dom F & j in dom (F . i) & k = (Sum (Card (F | (i -' 1)))) + j & (F . i) . j = (FlattenSeq F) . k )