theorem Th7: :: PELLS_EQ:7

for n, D being Nat ex F being FinSequence of NAT st
( len F = n + 1 & ( for k being Nat st k in dom F holds
F . k = [\((k - 1) * (sqrt D))/] + 1 ) & ( not D is square implies F is one-to-one ) )