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