:: deftheorem Def1 defines Fib PRE_FF:def 1 :
for b₁ being sequence of [:NAT,NAT:] holds
( b₁ = Fib iff ( b₁ . 0 = [0,1] & ( for n being Nat holds b₁ . (n + 1) = [((b₁ . n) `2),(((b<sub>1</sub> . n) `1) + ((b₁ . n) `2))] ) ) );