deffunc H₁( 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) = H<sub>1</sub>(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