И теория категорий здесь кажется нужна разве что чтобы его сформулировать и сэкономить 2 строчки на каждую структуру.
В принципе да. Но ведь не всегда стрелка - это функция. И изоморфизм в этой теореме понимается в категорном смысле (как обратимая стрелка). Поэтому гипотетически, если рассмотреть какую-нибудь хитрую категорию, где стрелками будут не просто функции, а, например, классы функций и хитро интерпретируемый изоморфизм, то я уже не уверен, будет ли "некатегорное" утверждение очевидным. Но в целом, так и есть. Даже я, только по сути начав читать теорию категорий, уже видел там много вещей, которые экономят гораздо больше строчек.
