Конструкция, использующая произвольный выбор

То, что я пытаюсь сейчас сделать — это примерно такая вещь. Допустим, мы хотим доказать изоморфизм V/W⊗U≅V⊗U/W⊗U для векторных пространств. Ну, по уму, понятно, нужно построить отображение слева направо или справа налево, потом уже любым способом проверять, что это изоморфизм. Но представим себе, что по уму мы не умеем почему-то. Тогда можно использовать такой дикий подход: выберем прямое дополнение T к W в V, тогда имеются изоморфизмы V/W≅T, откуда V/W⊗U≅T⊗U, и V≅W⊕T, откуда V⊗U≅W⊗U⊕T⊗U и V⊗U/W⊗U≅T⊗U. Искомый изоморфизм построен, осталось проверить, что он не зависит от выбора дополнительного подпространства T. В самом деле, пусть T′ — другое дополнительное подпространство к W в V; тогда… Казалось бы, это сущее безумие; так жить нельзя. Но никаких лучших идей в моей ситуации не просматривается. Вот, например.