theorem NF110: :: BINPACK1:6

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