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