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 Function of NAT ,[:NAT ,NAT :] such that
A1: L . 0 = [a,b] and
A2: for n being Nat holds L . (n + 1) = H<sub>1</sub>(n,L . n) from NAT_1:sch 12();
thus GenFib a,b,0 = [a,b] `1 by A1, A2, Def2
.= a by MCART_1:7 ; :: 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
.= [a,b] `2 by A1, MCART_1:7
.= b by MCART_1:7 ; :: 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 by MCART_1:7 ;
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 + 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
.= (GenFib a,b,n) + ((L . (n + 1)) `1 ) by A1, A2, 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