:: deftheorem Def5 defines Special_Function4 BOR_CANT:def 5 :
for n1, n2 being Nat
for b₃ being sequence of NAT holds
( b₃ = Special_Function4 (n1,n2) iff for n being Nat holds b₃ . n = IFGT (n,(n1 + 1),(n + n2),n) );