for c being XFinSequence of REAL st len c = 0 holds
for x being Nat holds (seq_p c) . x = 0