deffunc H1( set , Element of [:NAT ,NAT :]) -> Element of K19(NAT ,NAT ) = [($2 `2 ),(($2 `1 ) + ($2 `2 ))];
consider L being Function of NAT ,[:NAT ,NAT :] such that
A1:
L . 0 = [2,1]
and
A2:
for n being Nat holds L . (n + 1) = H1(n,L . n)
from NAT_1:sch 12();
thus Lucas 0 =
[2,1] `1
by A1, A2, Def1
.=
2
by MCART_1:7
; :: thesis: ( Lucas 1 = 1 & ( for n being Nat holds Lucas ((n + 1) + 1) = (Lucas n) + (Lucas (n + 1)) ) )
thus Lucas 1 =
(L . (0 + 1)) `1
by A1, A2, Def1
.=
[((L . 0 ) `2 ),(((L . 0 ) `1 ) + ((L . 0 ) `2 ))] `1
by A2
.=
[2,1] `2
by A1, MCART_1:7
.=
1
by MCART_1:7
; :: thesis: for n being Nat holds Lucas ((n + 1) + 1) = (Lucas n) + (Lucas (n + 1))
let n be Nat; :: thesis: Lucas ((n + 1) + 1) = (Lucas n) + (Lucas (n + 1))
A3: (L . (n + 1)) `1 =
[((L . n) `2 ),(((L . n) `1 ) + ((L . n) `2 ))] `1
by A2
.=
(L . n) `2
by MCART_1:7
;
thus Lucas ((n + 1) + 1) =
(L . ((n + 1) + 1)) `1
by A1, A2, Def1
.=
[((L . (n + 1)) `2 ),(((L . (n + 1)) `1 ) + ((L . (n + 1)) `2 ))] `1
by A2
.=
(L . (n + 1)) `2
by MCART_1:7
.=
[((L . n) `2 ),(((L . n) `1 ) + ((L . n) `2 ))] `2
by A2
.=
((L . n) `1 ) + ((L . (n + 1)) `1 )
by A3, MCART_1:7
.=
(Lucas n) + ((L . (n + 1)) `1 )
by A1, A2, Def1
.=
(Lucas n) + (Lucas (n + 1))
by A1, A2, Def1
; :: thesis: verum