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