let x, y, P, Q be Integer; :: thesis: ( 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))) ) )
set L = Lucas_Sequence (x,y,P,Q);
thus Lucas (x,y,P,Q,0) = [x,y] `1 by Def3
.= x ; :: thesis: ( 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))) ) )
thus Lucas (x,y,P,Q,1) = ((Lucas_Sequence (x,y,P,Q)) . (0 + 1)) `1
.= [(((Lucas_Sequence (x,y,P,Q)) . 0) `2),((P * (((Lucas_Sequence (x,y,P,Q)) . 0) `2)) - (Q * (((Lucas_Sequence (x,y,P,Q)) . 0) `1)))] `1 by Def3
.= [x,y] `2 by Def3
.= y ; :: thesis: 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)))
let n be Nat; :: thesis: Lucas (x,y,P,Q,(n + 2)) = (P * (Lucas (x,y,P,Q,(n + 1)))) - (Q * (Lucas (x,y,P,Q,n)))
A1: ((Lucas_Sequence (x,y,P,Q)) . (n + 1)) `1 = [(((Lucas_Sequence (x,y,P,Q)) . n) `2),((P * (((Lucas_Sequence (x,y,P,Q)) . n) `2)) - (Q * (((Lucas_Sequence (x,y,P,Q)) . n) `1)))] `1 by Def3
.= ((Lucas_Sequence (x,y,P,Q)) . n) `2 ;
n + 2 = (n + 1) + 1 ;
hence Lucas (x,y,P,Q,(n + 2)) = [(((Lucas_Sequence (x,y,P,Q)) . (n + 1)) `2),((P * (((Lucas_Sequence (x,y,P,Q)) . (n + 1)) `2)) - (Q * (((Lucas_Sequence (x,y,P,Q)) . (n + 1)) `1)))] `1 by Def3
.= [(((Lucas_Sequence (x,y,P,Q)) . n) `2),((P * (((Lucas_Sequence (x,y,P,Q)) . n) `2)) - (Q * (((Lucas_Sequence (x,y,P,Q)) . n) `1)))] `2 by Def3
.= (P * (Lucas (x,y,P,Q,(n + 1)))) - (Q * (Lucas (x,y,P,Q,n))) by A1 ;
:: thesis: verum