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

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