let C, D be Category; :: thesis: for S being Contravariant_Functor of C,D
for f being Morphism of C holds
( (Obj S) . (dom f) = cod (S . f) & (Obj S) . (cod f) = dom (S . f) )
let S be Contravariant_Functor of C,D; :: thesis: for f being Morphism of C holds
( (Obj S) . (dom f) = cod (S . f) & (Obj S) . (cod f) = dom (S . f) )
let f be Morphism of C; :: thesis: ( (Obj S) . (dom f) = cod (S . f) & (Obj S) . (cod f) = dom (S . f) )
( S . (id (dom f)) = id (cod (S . f)) & S . (id (cod f)) = id (dom (S . f)) ) by Def9;
hence ( (Obj S) . (dom f) = cod (S . f) & (Obj S) . (cod f) = dom (S . f) ) by Th28; :: thesis: verum