let C, D be Category; :: thesis: for T being Functor of C,D
for f being Morphism of C holds
( (Obj T) . (dom f) = dom (T . f) & (Obj T) . (cod f) = cod (T . f) )
let T be Functor of C,D; :: thesis: for f being Morphism of C holds
( (Obj T) . (dom f) = dom (T . f) & (Obj T) . (cod f) = cod (T . f) )
let f be Morphism of C; :: thesis: ( (Obj T) . (dom f) = dom (T . f) & (Obj T) . (cod f) = cod (T . f) )
( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) by Def19;
hence ( (Obj T) . (dom f) = dom (T . f) & (Obj T) . (cod f) = cod (T . f) ) by Th62; :: thesis: verum