deffunc H₁( set , Element of [:NAT,NAT:]) -> Element of [:NAT,NAT:] = [($2 `2),(($2 `1) + ($2 `2))];
consider L being sequence of [: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 ; :: 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
.= 1 ; :: 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 ;
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
.= [((L . n) `2),(((L . n) `1) + ((L . n) `2))] `2 by A2
.= ((L . n) `1) + ((L . (n + 1)) `1) by A3
.= (Lucas n) + ((L . (n + 1)) `1) by A1, A2, Def1
.= (Lucas n) + (Lucas (n + 1)) by A1, A2, Def1 ; :: thesis: verum