let A, B be Category; :: thesis: for F being Functor of A,B
for a, b, c being Object of A st Hom (a,b) <> {} & Hom (b,c) <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds F /. (g * f) = (F /. g) * (F /. f)
let F be Functor of A,B; :: thesis: for a, b, c being Object of A st Hom (a,b) <> {} & Hom (b,c) <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds F /. (g * f) = (F /. g) * (F /. f)
let a, b, c be Object of A; :: thesis: ( Hom (a,b) <> {} & Hom (b,c) <> {} implies for f being Morphism of a,b
for g being Morphism of b,c holds F /. (g * f) = (F /. g) * (F /. f) )
assume that
A1: Hom (a,b) <> {} and
A2: Hom (b,c) <> {} ; :: thesis: for f being Morphism of a,b
for g being Morphism of b,c holds F /. (g * f) = (F /. g) * (F /. f)
let f be Morphism of a,b; :: thesis: for g being Morphism of b,c holds F /. (g * f) = (F /. g) * (F /. f)
let g be Morphism of b,c; :: thesis: F /. (g * f) = (F /. g) * (F /. f)
A3: dom g = b by A2, CAT_1:5;
A4: cod f = b by A1, CAT_1:5;
A5: F /. g = F . g by A2, CAT_3:def 10;
A6: Hom ((F . a),(F . b)) <> {} by A1, CAT_1:84;
A7: F /. f = F . f by A1, CAT_3:def 10;
A8: Hom ((F . b),(F . c)) <> {} by A2, CAT_1:84;
Hom (a,c) <> {} by A1, A2, CAT_1:24;
hence F /. (g * f) = F . (g * f) by CAT_3:def 10
.= F . (g (*) f) by A1, A2, CAT_1:def 13
.= (F . g) (*) (F . f) by A3, A4, CAT_1:64
.= (F /. g) * (F /. f) by A6, A8, A5, A7, CAT_1:def 13 ;
:: thesis: verum