let L1, L2 be sequence of [:INT,INT:]; :: thesis: ( L1 . 0 = [x,y] & ( for n being Nat holds L1 . (n + 1) = [((L1 . n) `2),((P * ((L1 . n) `2)) - (Q * ((L1 . n) `1)))] ) & L2 . 0 = [x,y] & ( for n being Nat holds L2 . (n + 1) = [((L2 . n) `2),((P * ((L2 . n) `2)) - (Q * ((L2 . n) `1)))] ) implies L1 = L2 )
assume that
A1: L1 . 0 = [x,y] and
A2: for n being Nat holds L1 . (n + 1) = H₁(n,L1 . n) and
A3: L2 . 0 = [x,y] and
A4: for n being Nat holds L2 . (n + 1) = H₁(n,L2 . n) ; :: thesis: L1 = L2
thus L1 = L2 from NAT_1:sch 16(A1, A2, A3, A4); :: thesis: verum