let L1, L2 be sequence of [:NAT,NAT:]; ( 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) = H1(n,L1 . n)
and
A6:
L2 . 0 = [2,1]
and
A7:
for n being Nat holds L2 . (n + 1) = H1(n,L2 . n)
; L1 = L2
thus
L1 = L2
from NAT_1:sch 16(A3, A4, A6, A7); verum