for M being MidSp holds vect M is_atlas_of the carrier of M, vectgroup M