deffunc H₁( set , Element of [:NAT,NAT:]) -> Element of [:NAT,NAT:] = In ([($2 `2),(($2 `1) + ($2 `2))],[:NAT,NAT:]);
let it1, it2 be Element of NAT ; :: thesis: ( ex fib being sequence of [: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 sequence of [: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 sequence of [: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) = [((fib1 . n) `2),(((fib1 . n) `1) + ((fib1 . n) `2))] ; :: thesis: ( for fib being sequence of [: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 )
A5: for n being Nat holds fib1 . (n + 1) = H<sub>1</sub>(n,fib1 . n) by A4;
given fib2 being sequence of [:NAT,NAT:] such that A6: it2 = (fib2 . n) `1 and
A7: fib2 . 0 = [0,1] and
A8: for n being Nat holds fib2 . (n + 1) = [((fib2 . n) `2),(((fib2 . n) `1) + ((fib2 . n) `2))] ; :: thesis: it1 = it2
A9: for n being Nat holds fib2 . (n + 1) = H₁(n,fib2 . n) by A8;
fib1 = fib2 from NAT_1:sch 16(A3, A5, A7, A9);
hence it1 = it2 by A2, A6; :: thesis: verum