for f being Element of the_set_of_RealSequences st ( for n being Nat holds (seq_id f) . n = 0 ) holds
f = Zeroseq