let C, D be Category; :: thesis: for F being Functor of C,D holds F is Functor of C, Image F
let F be Functor of C,D; :: thesis: F is Functor of C, Image F
rng F c= the carrier' of (Image F) by Def3;
hence F is Functor of C, Image F by Th7; :: thesis: verum