let A, B, C be Category; ( A,B are_equivalent & B,C are_equivalent implies A,C are_equivalent )
given F1 being Functor of A,B, G1 being Functor of B,A such that A1:
G1 * F1 ~= id A
and
A2:
F1 * G1 ~= id B
; ISOCAT_1:def 10 ( not B,C are_equivalent or A,C are_equivalent )
given F2 being Functor of B,C, G2 being Functor of C,B such that A3:
G2 * F2 ~= id B
and
A4:
F2 * G2 ~= id C
; ISOCAT_1:def 10 A,C are_equivalent
take
F2 * F1
; ISOCAT_1:def 10 ex G being Functor of C,A st
( G * (F2 * F1) ~= id A & (F2 * F1) * G ~= id C )
take
G1 * G2
; ( (G1 * G2) * (F2 * F1) ~= id A & (F2 * F1) * (G1 * G2) ~= id C )
(G1 * G2) * F2 = G1 * (G2 * F2)
by RELAT_1:36;
then A5:
(G1 * G2) * F2 ~= G1
by A3, Th42;
(G1 * G2) * (F2 * F1) = ((G1 * G2) * F2) * F1
by RELAT_1:36;
then
(G1 * G2) * (F2 * F1) ~= G1 * F1
by A5, Th41;
hence
(G1 * G2) * (F2 * F1) ~= id A
by A1, NATTRA_1:29; (F2 * F1) * (G1 * G2) ~= id C
(F2 * F1) * G1 = F2 * (F1 * G1)
by RELAT_1:36;
then A6:
(F2 * F1) * G1 ~= F2
by A2, Th42;
(F2 * F1) * (G1 * G2) = ((F2 * F1) * G1) * G2
by RELAT_1:36;
then
(F2 * F1) * (G1 * G2) ~= F2 * G2
by A6, Th41;
hence
(F2 * F1) * (G1 * G2) ~= id C
by A4, NATTRA_1:29; verum