:: deftheorem Def3 defines Lucas_Sequence NOMIN_9:def 3 :
for x, y, P, Q being Integer
for b₅ being sequence of [:INT,INT:] holds
( b₅ = Lucas_Sequence (x,y,P,Q) iff ( b₅ . 0 = [x,y] & ( for n being Nat holds b₅ . (n + 1) = [((b₅ . n) `2),((P * ((b<sub>5</sub> . n) `2)) - (Q * ((b₅ . n) `1)))] ) ) );