:: deftheorem Def2 defines Fusc PRE_FF:def 3 :
for n being Nat
for b₂ being Element of NAT holds
( ( n = 0 implies ( b₂ = Fusc n iff b₂ = 0 ) ) & ( not n = 0 implies ( b₂ = Fusc n iff ex l being Element of NAT ex fusc being sequence of (NAT *) st
( l + 1 = n & b₂ = (fusc . l) /. n & fusc . 0 = <*1*> & ( for n being Nat holds
( ( for k being Nat st n + 2 = 2 * k holds
fusc . (n + 1) = (fusc . n) ^ <*((fusc . n) /. k)*> ) & ( for k being Nat st n + 2 = (2 * k) + 1 holds
fusc . (n + 1) = (fusc . n) ^ <*(((fusc . n) /. k) + ((fusc . n) /. (k + 1)))*> ) ) ) ) ) ) );