for x being Nat holds seq . x = 0 ;
hence Sum seq is zero by RSSPACE:16; :: thesis: verum