:: deftheorem defines Lucas NOMIN_9:def 4 :
for x, y, P, Q being Integer
for n being Nat holds Lucas (x,y,P,Q,n) = ((Lucas_Sequence (x,y,P,Q)) . n) `1 ;