:: deftheorem Def4 defines Special_Function3 BOR_CANT:def 4 :
for k being Nat
for b₂ being sequence of NAT holds
( b₂ = Special_Function3 k iff for n being Nat holds b₂ . n = IFGT (n,k,0,1) );