let A, B, C be Category; :: thesis: ( 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 ; :: according to ISOCAT_1:def 10 :: thesis: ( 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 ; :: according to ISOCAT_1:def 10 :: thesis: A,C are_equivalent
take F2 * F1 ; :: according to ISOCAT_1:def 10 :: thesis: ex G being Functor of C,A st
( G * (F2 * F1) ~= id A & (F2 * F1) * G ~= id C )
take G1 * G2 ; :: thesis: ( (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; :: thesis: (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; :: thesis: verum