:: deftheorem Def2 defines FIB FIB_NUM2:def 2 :
for b₁ being sequence of NAT holds
( b₁ = FIB iff for k being Element of NAT holds b₁ . k = Fib k );