deffunc H_{2}( 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_{2}(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

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

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