for n being Nat holds Sum (n |-> (0. Z_2)) = 0. Z_2