theorem Th4: :: NBVECTSP:4

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