let C, D be Category; :: thesis: for T being Functor of C,D
for a, b, c being Object of C st Hom (a,b) <> {} & Hom (b,c) <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds T /. (g * f) = (T /. g) * (T /. f)

let T be Functor of C,D; :: thesis: for a, b, c being Object of C st Hom (a,b) <> {} & Hom (b,c) <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds T /. (g * f) = (T /. g) * (T /. f)

let a, b, c be Object of C; :: thesis: ( Hom (a,b) <> {} & Hom (b,c) <> {} implies for f being Morphism of a,b
for g being Morphism of b,c holds T /. (g * f) = (T /. g) * (T /. f) )

assume A1: ( Hom (a,b) <> {} & Hom (b,c) <> {} ) ; :: thesis: for f being Morphism of a,b
for g being Morphism of b,c holds T /. (g * f) = (T /. g) * (T /. f)

let f be Morphism of a,b; :: thesis: for g being Morphism of b,c holds T /. (g * f) = (T /. g) * (T /. f)
let g be Morphism of b,c; :: thesis: T /. (g * f) = (T /. g) * (T /. f)
A2: cod f = b by
.= dom g by ;
reconsider gg = g, ff = f as Morphism of C ;
A3: Hom (a,c) <> {} by ;
A4: T /. g = T . gg by ;
A5: T /. f = T . ff by ;
A6: ( Hom ((T . a),(T . b)) <> {} & Hom ((T . b),(T . c)) <> {} ) by ;
g * f = gg (*) ff by ;
hence T /. (g * f) = T . (gg (*) ff) by
.= (T . gg) (*) (T . ff) by
.= (T /. g) * (T /. f) by ;
:: thesis: verum