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 12;
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