let A, B, C, D be Category; :: thesis: ( A ~= B & C ~= D implies [:A,C:] ~= [:B,D:] )
given F being Functor of A,B such that A1: F is isomorphic ; :: according to ISOCAT_1:def 4 :: thesis: ( not C ~= D or [:A,C:] ~= [:B,D:] )
given G being Functor of C,D such that A2: G is isomorphic ; :: according to ISOCAT_1:def 4 :: thesis: [:A,C:] ~= [:B,D:]
take [:F,G:] ; :: according to ISOCAT_1:def 4 :: thesis: [:F,G:] is isomorphic
( F is one-to-one & G is one-to-one ) by A1, A2, Def3;
hence [:F,G:] is one-to-one by Th1; :: according to ISOCAT_1:def 3 :: thesis: rng [:F,G:] = the carrier' of [:B,D:]
thus rng [:F,G:] = [:(rng F),(rng G):] by FUNCT_3:88
.= [:the carrier' of B,(rng G):] by A1, Def3
.= the carrier' of [:B,D:] by A2, Def3 ; :: thesis: verum