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:] )
A2: F is one-to-one by A1;
given G being Functor of C,D such that A3: 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
G is one-to-one by A3;
hence [:F,G:] is one-to-one by A2; :: 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:67
.= [: the carrier' of B,(rng G):] by A1
.= the carrier' of [:B,D:] by A3 ; :: thesis: verum