let A, B, C be Category; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: according to ISOCAT_1:def 3 :: thesis: G * F is isomorphic
thus G * F is one-to-one by A1, A3, FUNCT_1:24; :: according to ISOCAT_1:def 3 :: thesis: 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; :: thesis: verum