let A, B, C be Category; :: thesis: ( A ~= B & B ~= C implies A ~= C )
given F1 being Functor of A,B such that A1: F1 is isomorphic ; :: according to ISOCAT_1:def 4 :: thesis: ( not B ~= C or A ~= C )
given F2 being Functor of B,C such that A2: F2 is isomorphic ; :: according to ISOCAT_1:def 4 :: thesis: A ~= C
take F2 * F1 ; :: according to ISOCAT_1:def 4 :: thesis: F2 * F1 is isomorphic
thus F2 * F1 is isomorphic by A1, A2, Th12; :: thesis: verum