let fib1, fib2 be sequence of [:NAT,NAT:]; :: thesis: ( fib1 . 0 = [0,1] & ( for n being Nat holds fib1 . (n + 1) = [((fib1 . n) `2),(((fib1 . n) `1) + ((fib1 . n) `2))] ) & fib2 . 0 = [0,1] & ( for n being Nat holds fib2 . (n + 1) = [((fib2 . n) `2),(((fib2 . n) `1) + ((fib2 . n) `2))] ) implies fib1 = fib2 )
assume that
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: ( not fib2 . 0 = [0,1] or ex n being Nat st not fib2 . (n + 1) = [((fib2 . n) `2),(((fib2 . n) `1) + ((fib2 . n) `2))] or fib1 = fib2 )
A5: for n being Nat holds fib1 . (n + 1) = H₁(n,fib1 . n) by A4;
assume that
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: fib1 = fib2
A9: for n being Nat holds fib2 . (n + 1) = H₁(n,fib2 . n) by A8;
thus fib1 = fib2 from NAT_1:sch 16(A3, A5, A7, A9); :: thesis: verum