deffunc H₁( set , Element of [:NAT,NAT:]) -> Element of [:NAT,NAT:] = [($2 `2),(($2 `1) + ($2 `2))];
reconsider n = n as Element of NAT by ORDINAL1:def 12;
consider fib being Function of NAT,[:NAT,NAT:] such that
A1: ( fib . 0 = [0,1] & ( for n being Nat holds fib . (n + 1) = H<sub>1</sub>(n,fib . n) ) ) from NAT_1:sch 12();
take (fib . n) `1 ; :: thesis: ex fib being Function of NAT,[:NAT,NAT:] st
( (fib . n) `1 = (fib . n) `1 & fib . 0 = [0,1] & ( for n being Nat holds fib . (n + 1) = [((fib . n) `2),(((fib . n) `1) + ((fib . n) `2))] ) )
take fib ; :: thesis: ( (fib . n) `1 = (fib . n) `1 & fib . 0 = [0,1] & ( for n being Nat holds fib . (n + 1) = [((fib . n) `2),(((fib . n) `1) + ((fib . n) `2))] ) )
thus ( (fib . n) `1 = (fib . n) `1 & fib . 0 = [0,1] & ( for n being Nat holds fib . (n + 1) = [((fib . n) `2),(((fib . n) `1) + ((fib . n) `2))] ) ) by A1; :: thesis: verum