let A, B, C be Category; :: thesis: for F being Functor of A,B
for G being Functor of B,C
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (G * F) /. f = G /. (F /. f)
let F be Functor of A,B; :: thesis: for G being Functor of B,C
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (G * F) /. f = G /. (F /. f)
let G be Functor of B,C; :: thesis: for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (G * F) /. f = G /. (F /. f)
let a, b be Object of A; :: thesis: ( Hom (a,b) <> {} implies for f being Morphism of a,b holds (G * F) /. f = G /. (F /. f) )
assume A1: Hom (a,b) <> {} ; :: thesis: for f being Morphism of a,b holds (G * F) /. f = G /. (F /. f)
then A2: Hom ((F . a),(F . b)) <> {} by CAT_1:84;
let f be Morphism of a,b; :: thesis: (G * F) /. f = G /. (F /. f)
thus (G * F) /. f = (G * F) . f by A1, CAT_3:def 10
.= G . (F . f) by FUNCT_2:15
.= G . (F /. f) by A1, CAT_3:def 10
.= G /. (F /. f) by A2, CAT_3:def 10 ; :: thesis: verum