ex L being sequence of [:INT,INT:] st
( L . 0 = [x,y] & ( for n being Nat holds L . (n + 1) = H₁(n,L . n) ) ) from NAT_1:sch 12();
hence ex b₁ being sequence of [:INT,INT:] st
( b₁ . 0 = [x,y] & ( for n being Nat holds b₁ . (n + 1) = [((b₁ . n) `2),((P * ((b<sub>1</sub> . n) `2)) - (Q * ((b₁ . n) `1)))] ) ) ; :: thesis: verum