for f being FinSequence of NAT
for j, b being Nat st b = j holds
(f ^ <*b*>) " {j} = (f " {j}) \/ {((len f) + 1)}