theorem Th19: :: EUCLID_7:20

for n being Nat holds {(0* n)} is linear_manifold