theorem :: FLEXARY1:6

for D being non empty set
for i being Nat
for f being FinSequence of D * holds
( i in dom ((D -concatenation) "**" f) iff ex n, k being Nat st
( n + 1 in dom f & k in dom (f . (n + 1)) & i = k + (len ((D -concatenation) "**" (f | n))) ) )