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