:: deftheorem Def2 defines GenFib FIB_NUM3:def 3 :
for a, b being Nat
for b₃ being sequence of [:NAT,NAT:] holds
( b₃ = GenFib (a,b) iff ( b₃ . 0 = [a,b] & ( for n being Nat holds b₃ . (n + 1) = [((b₃ . n) `2),(((b<sub>3</sub> . n) `1) + ((b₃ . n) `2))] ) ) );