:: deftheorem Def2 defines Fusc' FIB_FUSC:def 2 :
for i being Integer
for b₂ being Element of NAT holds
( b₂ = Fusc' i iff ( ex n being Element of NAT st
( i = n & b₂ = Fusc n ) or ( i is not Element of NAT & b₂ = 0 ) ) );