deffunc H₁( set , Element of [:NAT ,NAT :]) -> Element of [:NAT ,NAT :] = [($2 `2 ),(($2 `1 ) + ($2 `2 ))];
let it1, it2 be Element of NAT ; :: thesis: ( ex fib being Function of NAT ,[:NAT ,NAT :] st
( it1 = (fib . n) `1 & fib . 0 = [0 ,1] & ( for n being Nat holds fib . (n + 1) = [((fib . n) `2 ),(((fib . n) `1 ) + ((fib . n) `2 ))] ) ) & ex fib being Function of NAT ,[:NAT ,NAT :] st
( it2 = (fib . n) `1 & fib . 0 = [0 ,1] & ( for n being Nat holds fib . (n + 1) = [((fib . n) `2 ),(((fib . n) `1 ) + ((fib . n) `2 ))] ) ) implies it1 = it2 )
given fib1 being Function of NAT ,[:NAT ,NAT :] such that A2: it1 = (fib1 . n) `1 and
A3: fib1 . 0 = [0 ,1] and
A4: for n being Nat holds fib1 . (n + 1) = H₁(n,fib1 . n) ; :: thesis: ( for fib being Function of NAT ,[:NAT ,NAT :] holds
( not it2 = (fib . n) `1 or not fib . 0 = [0 ,1] or ex n being Nat st not fib . (n + 1) = [((fib . n) `2 ),(((fib . n) `1 ) + ((fib . n) `2 ))] ) or it1 = it2 )
given fib2 being Function of NAT ,[:NAT ,NAT :] such that A5: it2 = (fib2 . n) `1 and
A6: fib2 . 0 = [0 ,1] and
A7: for n being Nat holds fib2 . (n + 1) = H₁(n,fib2 . n) ; :: thesis: it1 = it2
fib1 = fib2 from NAT_1:sch 16(A3, A4, A6, A7);
hence it1 = it2 by A2, A5; :: thesis: verum