for d being XFinSequence of REAL
for k being Nat st len d = k + 1 holds
ex a being Real ex d1 being XFinSequence of REAL ex y being Real_Sequence st
( len d1 = k & d1 = d | k & a = d . k & d = d1 ^ <%a%> & seq_p d = (seq_p d1) + y & ( for i being Nat holds y . i = a * (i to_power k) ) )