theorem :: NOMIN_9:11

for n being Nat holds Lucas (2,1,1,(- 1),n) = Lucas n by Th10;