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