:: deftheorem Def2 defines GenFib FIB_NUM3:def 2 :
for a, b, n being Nat
for b₄ being Element of NAT holds
( b₄ = GenFib (a,b,n) iff ex L being sequence of [:NAT,NAT:] st
( b₄ = (L . n) `1 & L . 0 = [a,b] & ( for n being Nat holds L . (n + 1) = [((L . n) `2),(((L . n) `1) + ((L . n) `2))] ) ) );