deffunc H₁( set , Element of [:NAT ,NAT :]) -> Element of [:NAT ,NAT :] = [($2 `2 ),(($2 `1 ) + ($2 `2 ))];
consider fib being Function of NAT ,[:NAT ,NAT :] such that
A1: fib . 0 = [0 ,1] and
A2: for n being Nat holds fib . (n + 1) = H<sub>1</sub>(n,fib . n) from NAT_1:sch 12();
thus Fib 0 = [0 ,1] `1 by A1, A2, Def1
.= 0 by MCART_1:7 ; :: thesis: ( Fib 1 = 1 & ( for n being Nat holds Fib ((n + 1) + 1) = (Fib n) + (Fib (n + 1)) ) )
thus Fib 1 = (fib . (0 + 1)) `1 by A1, A2, Def1
.= [((fib . 0 ) `2 ),(((fib . 0 ) `1 ) + ((fib . 0 ) `2 ))] `1 by A2
.= [0 ,1] `2 by A1, MCART_1:7
.= 1 by MCART_1:7 ; :: thesis: for n being Nat holds Fib ((n + 1) + 1) = (Fib n) + (Fib (n + 1))
let n be Nat; :: thesis: Fib ((n + 1) + 1) = (Fib n) + (Fib (n + 1))
reconsider n = n as Element of NAT by ORDINAL1:def 13;
A3: (fib . (n + 1)) `1 = [((fib . n) `2 ),(((fib . n) `1 ) + ((fib . n) `2 ))] `1 by A2
.= (fib . n) `2 by MCART_1:7 ;
Fib ((n + 1) + 1) = (fib . ((n + 1) + 1)) `1 by A1, A2, Def1
.= [((fib . (n + 1)) `2 ),(((fib . (n + 1)) `1 ) + ((fib . (n + 1)) `2 ))] `1 by A2
.= (fib . (n + 1)) `2 by MCART_1:7
.= [((fib . n) `2 ),(((fib . n) `1 ) + ((fib . n) `2 ))] `2 by A2
.= ((fib . n) `1 ) + ((fib . (n + 1)) `1 ) by A3, MCART_1:7
.= (Fib n) + ((fib . (n + 1)) `1 ) by A1, A2, Def1
.= (Fib n) + (Fib (n + 1)) by A1, A2, Def1 ;
hence Fib ((n + 1) + 1) = (Fib n) + (Fib (n + 1)) ; :: thesis: verum