set L = Lucas_Sequence (2,1,1,(- 1));
set F = Lucas ;
( dom Lucas = NAT & dom (Lucas_Sequence (2,1,1,(- 1))) = NAT )
by FUNCT_2:def 1;
hence
dom (Lucas_Sequence (2,1,1,(- 1))) = dom Lucas
; FUNCT_1:def 11 for b1 being object holds
( not b1 in dom (Lucas_Sequence (2,1,1,(- 1))) or (Lucas_Sequence (2,1,1,(- 1))) . b1 = Lucas . b1 )
let n be object ; ( not n in dom (Lucas_Sequence (2,1,1,(- 1))) or (Lucas_Sequence (2,1,1,(- 1))) . n = Lucas . n )
assume A1:
n in dom (Lucas_Sequence (2,1,1,(- 1)))
; (Lucas_Sequence (2,1,1,(- 1))) . n = Lucas . n
defpred S1[ Nat] means (Lucas_Sequence (2,1,1,(- 1))) . $1 = Lucas . $1;
(Lucas_Sequence (2,1,1,(- 1))) . 0 = [2,1]
by Def3;
then A2:
S1[ 0 ]
by FIB_NUM3:def 1;
A3:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A4:
S1[
k]
;
S1[k + 1]
thus (Lucas_Sequence (2,1,1,(- 1))) . (k + 1) =
[(((Lucas_Sequence (2,1,1,(- 1))) . k) `2),((1 * (((Lucas_Sequence (2,1,1,(- 1))) . k) `2)) - ((- 1) * (((Lucas_Sequence (2,1,1,(- 1))) . k) `1)))]
by Def3
.=
[((Lucas . k) `2),(((Lucas . k) `1) + ((Lucas . k) `2))]
by A4
.=
Lucas . (k + 1)
by FIB_NUM3:def 1
;
verum
end;
for k being Nat holds S1[k]
from NAT_1:sch 2(A2, A3);
hence
(Lucas_Sequence (2,1,1,(- 1))) . n = Lucas . n
by A1; verum