reconsider n = n as Element of NAT by ORDINAL1:def 13;
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();
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, A2; :: thesis: verum