Ну да (по модулю того, что компактность хитро запрятана под ковер в утверждение про базис окрестностей, которое приводится без доказательства -- а может она и не нужна вообще).

В принципе, если ты хочешь концептуальной полной ясности, то она такая: имеется понятие C^\infty-кольца. Неформально, это кольцо, в котором элементы мохно подставлять в гладкие функции na R (а не только в полиномы). Формально, это мн-во X плюс мультилинейные операции, а операции из X^n в X^m это гладкие отображения из R^n в R^m. Ну и такие уже более-менее отвечают многообразиям (не все, но категория многообразий туда вкладывается полно и строго). Не уверен, что это надо объяснять студентам, особенно уже испорченны излишней алгеброй. Но все же.