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 A1, CAT_1:5
.= dom g by A1, CAT_1:5 ;
reconsider gg = g, ff = f as Morphism of C ;
A3: Hom (a,c) <> {} by A1, CAT_1:24;
A4: T /. g = T . gg by Def10, A1;
A5: T /. f = T . ff by Def10, A1;
A6: ( Hom ((T . a),(T . b)) <> {} & Hom ((T . b),(T . c)) <> {} ) by A1, CAT_1:84;
g * f = gg (*) ff by A1, CAT_1:def 13;
hence T /. (g * f) = T . (gg (*) ff) by Def10, A3
.= (T . gg) (*) (T . ff) by A2, CAT_1:64
.= (T /. g) * (T /. f) by A6, A4, A5, CAT_1:def 13 ;
:: thesis: verum