for k being Nat
for D being non empty set
for sq being FinSequence of D st 1 <= k & k < len sq holds
(sq /^ 1) . k = sq . (k + 1)