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 id (dom (T . g)) = T . (id (cod f)) by Def18
.= id (cod (T . f)) by Def18 ;
hence dom (T . g) = cod (T . f) by Th45; :: thesis: T . (g * f) = (T . g) * (T . f)
then ( the Comp of C . g,f = g * f & the Comp of D . (T . g),(T . f) = (T . g) * (T . f) & [g,f] in dom the Comp of C ) by A1, Def8, Th41;
hence T . (g * f) = (T . g) * (T . f) by Def18; :: thesis: verum