for n being Nat
for fp being FinSequence of INT st len fp = n + 2 holds
for a being Integer ex fr being FinSequence of INT ex r being Integer st
( len fr = n + 1 & ( for x being Element of INT holds (Poly-INT fp) . x = ((x - a) * ((Poly-INT fr) . x)) + r ) & fp . (n + 2) = fr . (n + 1) )