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

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