deffunc H₁( set , Element of [:NAT,NAT:]) -> Element of [:NAT,NAT:] = In ([($2 `2),(($2 `1) + ($2 `2))],[:NAT,NAT:]);
consider fib being sequence of [: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();
A3: for n being Nat holds fib . (n + 1) = [((fib . n) `2),(((fib . n) `1) + ((fib . n) `2))]

proof

let n be Nat; :: thesis: fib . (n + 1) = [((fib . n) `2),(((fib . n) `1) + ((fib . n) `2))]
reconsider i = (fib . n) `2 , j = ((fib . n) `1) + ((fib . n) `2) as Nat ;
fib . (n + 1) = H₁(n,fib . n) by A2
.= [i,j] ;
hence fib . (n + 1) = [((fib . n) `2),(((fib . n) `1) + ((fib . n) `2))] ; :: thesis: verum

end;

thus Fib 0 = [0,1] `1 by A1, A3, Def1
.= 0 ; :: 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, A3, Def1
.= [((fib . 0) `2),(((fib . 0) `1) + ((fib . 0) `2))] `1 by A3
.= [0,1] `2 by A1
.= 1 ; :: 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;
A4: (fib . (n + 1)) `1 = [((fib . n) `2),(((fib . n) `1) + ((fib . n) `2))] `1 by A3
.= (fib . n) `2 ;
Fib ((n + 1) + 1) = (fib . ((n + 1) + 1)) `1 by A1, A3, Def1
.= [((fib . (n + 1)) `2),(((fib . (n + 1)) `1) + ((fib . (n + 1)) `2))] `1 by A3
.= (fib . (n + 1)) `2
.= [((fib . n) `2),(((fib . n) `1) + ((fib . n) `2))] `2 by A3
.= ((fib . n) `1) + ((fib . (n + 1)) `1) by A4
.= (Fib n) + ((fib . (n + 1)) `1) by A1, A3, Def1
.= (Fib n) + (Fib (n + 1)) by A1, A3, Def1 ;
hence Fib ((n + 1) + 1) = (Fib n) + (Fib (n + 1)) ; :: thesis: verum