let C, D be Category; :: thesis: for S being Contravariant_Functor of C,D
for f, g being Morphism of C st dom g = cod f holds
dom (S . f) = cod (S . g)
let S be Contravariant_Functor of C,D; :: thesis: for f, g being Morphism of C st dom g = cod f holds
dom (S . f) = cod (S . g)
let f, g be Morphism of C; :: thesis: ( dom g = cod f implies dom (S . f) = cod (S . g) )
assume dom g = cod f ; :: thesis: dom (S . f) = cod (S . g)
hence dom (S . f) = (Obj S) . (dom g) by Th30
.= cod (S . g) by Th30 ;
:: thesis: verum