let C, D be Category; :: thesis: for T being Functor of C,D
for f, g being Morphism of C st dom g = cod f holds
( dom (T . g) = cod (T . f) & T . (g (*) f) = (T . g) (*) (T . f) )
let T be Functor of C,D; :: thesis: for f, g being Morphism of C st dom g = cod f holds
( dom (T . g) = cod (T . f) & T . (g (*) f) = (T . g) (*) (T . f) )
let f, g be Morphism of C; :: thesis: ( dom g = cod f implies ( dom (T . g) = cod (T . f) & T . (g (*) f) = (T . g) (*) (T . f) ) )
assume A1: dom g = cod f ; :: thesis: ( dom (T . g) = cod (T . f) & T . (g (*) f) = (T . g) (*) (T . f) )
then A2: ( the Comp of C . (g,f) = g (*) f & [g,f] in dom the Comp of C ) by Def4, Th14;
id (dom (T . g)) = T . (id (cod f)) by A1, Def19
.= id (cod (T . f)) by Def19 ;
hence dom (T . g) = cod (T . f) by Th54; :: thesis: T . (g (*) f) = (T . g) (*) (T . f)
thus T . (g (*) f) = (T . g) (*) (T . f) by A2, Def19; :: thesis: verum