:: deftheorem Def3 defines Special_Function2 BOR_CANT:def 3 :
for k being Nat
for b₂ being sequence of NAT holds
( b₂ = Special_Function2 k iff for n being Nat holds b₂ . n = n + k );