:: deftheorem Def2 defines Special_Function BOR_CANT:def 2 :
for n1, n2 being Nat
for b₃ being sequence of NAT holds
( b₃ = Special_Function (n1,n2) iff for n being Nat holds b₃ . n = IFGT (n,n1,(n + n2),n) );