for d being XFinSequence of REAL
for k being Nat st len d = 1 holds
ex a being Real st
( a = d . 0 & ( for x being Nat holds (seq_p d) . x = a ) )