let L1, L2 be sequence of [:NAT,NAT:]; :: thesis: ( L1 . 0 = [2,1] & ( for n being Nat holds L1 . (n + 1) = [((L1 . n) `2),(((L1 . n) `1) + ((L1 . n) `2))] ) & L2 . 0 = [2,1] & ( for n being Nat holds L2 . (n + 1) = [((L2 . n) `2),(((L2 . n) `1) + ((L2 . n) `2))] ) implies L1 = L2 )

assume that

A3: L1 . 0 = [2,1] and

A4: for n being Nat holds L1 . (n + 1) = H_{1}(n,L1 . n)
and

A6: L2 . 0 = [2,1] and

A7: for n being Nat holds L2 . (n + 1) = H_{1}(n,L2 . n)
; :: thesis: L1 = L2

thus L1 = L2 from NAT_1:sch 16(A3, A4, A6, A7); :: thesis: verum

assume that

A3: L1 . 0 = [2,1] and

A4: for n being Nat holds L1 . (n + 1) = H

A6: L2 . 0 = [2,1] and

A7: for n being Nat holds L2 . (n + 1) = H

thus L1 = L2 from NAT_1:sch 16(A3, A4, A6, A7); :: thesis: verum