deffunc H₂( set , Element of [:NAT,NAT:]) -> Element of [:NAT,NAT:] = [($2 `2),(($2 `1) + ($2 `2))];
let a, b be Nat; :: thesis: ( GenFib (a,b,0) = a & GenFib (a,b,1) = b & ( for n being Nat holds GenFib (a,b,((n + 1) + 1)) = (GenFib (a,b,n)) + (GenFib (a,b,(n + 1))) ) )
consider L being sequence of [:NAT,NAT:] such that
A1: L . 0 = [a,b] and
A2: for n being Nat holds L . (n + 1) = H<sub>2</sub>(n,L . n) from NAT_1:sch 12();
thus GenFib (a,b,0) = [a,b] `1 by Def2
.= a ; :: thesis: ( GenFib (a,b,1) = b & ( for n being Nat holds GenFib (a,b,((n + 1) + 1)) = (GenFib (a,b,n)) + (GenFib (a,b,(n + 1))) ) )
thus GenFib (a,b,1) = (L . (0 + 1)) `1 by A1, A2, Def2
.= [((L . 0) `2),(((L . 0) `1) + ((L . 0) `2))] `1 by A2
.= b by A1 ; :: thesis: for n being Nat holds GenFib (a,b,((n + 1) + 1)) = (GenFib (a,b,n)) + (GenFib (a,b,(n + 1)))
let n be Nat; :: thesis: GenFib (a,b,((n + 1) + 1)) = (GenFib (a,b,n)) + (GenFib (a,b,(n + 1)))
A3: (L . (n + 1)) `1 = [((L . n) `2),(((L . n) `1) + ((L . n) `2))] `1 by A2
.= (L . n) `2 ;
GenFib (a,b,((n + 1) + 1)) = (L . ((n + 1) + 1)) `1 by A1, A2, Def2
.= [((L . (n + 1)) `2),(((L . (n + 1)) `1) + ((L . (n + 1)) `2))] `1 by A2
.= [((L . n) `2),(((L . n) `1) + ((L . n) `2))] `2 by A2
.= (GenFib (a,b,n)) + ((L . (n + 1)) `1) by A1, A2, A3, Def2
.= (GenFib (a,b,n)) + (GenFib (a,b,(n + 1))) by A1, A2, Def2 ;
hence GenFib (a,b,((n + 1) + 1)) = (GenFib (a,b,n)) + (GenFib (a,b,(n + 1))) ; :: thesis: verum