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