theorem Th5: :: NOMIN_9:5

for x, y, P, Q being Integer holds
( Lucas (x,y,P,Q,0) = x & Lucas (x,y,P,Q,1) = y & ( for n being Nat holds Lucas (x,y,P,Q,(n + 2)) = (P * (Lucas (x,y,P,Q,(n + 1)))) - (Q * (Lucas (x,y,P,Q,n))) ) )