let A, B, C be Category; for F being Functor of A,B
for G being Functor of B,C st F is isomorphic & G is isomorphic holds
G * F is isomorphic
let F be Functor of A,B; for G being Functor of B,C st F is isomorphic & G is isomorphic holds
G * F is isomorphic
let G be Functor of B,C; ( F is isomorphic & G is isomorphic implies G * F is isomorphic )
assume that
A1:
F is one-to-one
and
A2:
rng F = the carrier' of B
and
A3:
G is one-to-one
and
A4:
rng G = the carrier' of C
; ISOCAT_1:def 3 G * F is isomorphic
thus
G * F is one-to-one
by A1, A3, FUNCT_1:24; ISOCAT_1:def 3 rng (G * F) = the carrier' of C
dom G = the carrier' of B
by FUNCT_2:def 1;
hence
rng (G * F) = the carrier' of C
by A2, A4, RELAT_1:28; verum