Прямое произведение -- это проективный предел диаграммы из двух точек: A и B. Кстати, обобщается на любое количество объектов, как их проективный предел.
Мне кажется, проще доказать, что

с точностью до единственного изоморфизма. Кстати, изоморфизм можно и не строить из-за специфики пределов. По сути, можно сказать, что объект

удовлетворяет диаграмме для проективного предела над

. Это проверяется визуально на диаграмме. Это и есть доказательство, ведь мы показали, что

является

, а значит они равны с точностью до уникального изоморфизма.
Аналогично,

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

нельзя говорить, в общем случае это неправильно. Но мы хотим мыслить произведение какой-то конкретной функцией, как мы это мыслим в конкретных категориях (Set,Vect,Top,...). Благо, мы так можем делать: если пределы и различны (формально), то всё равно мы можем все рассуждения перенести, используя данный нам единственный изоморфизм.