theorem :: RSSPACE:4

for n being object holds (seq_id Zeroseq) . n = 0