:: deftheorem Def2 defines ^\ NAT_1:def 2 :
for s being ManySortedSet of NAT
for k being natural Number
for b₃ being ManySortedSet of NAT holds
( b₃ = s ^\ k iff for n being Nat holds b₃ . n = s . (n + k) );