let A, B be Category; :: thesis: for F being Functor of A,B st F is isomorphic holds
F " is isomorphic
let F be Functor of A,B; :: thesis: ( F is isomorphic implies F " is isomorphic )
assume F is isomorphic ; :: thesis: F " is isomorphic
then A1: ( F is one-to-one & F " = F " ) by Def2;
hence F " is one-to-one by FUNCT_1:40; :: according to ISOCAT_1:def 3 :: thesis: rng (F ") = the carrier' of A
thus rng (F ") = dom F by A1, FUNCT_1:33
.= the carrier' of A by FUNCT_2:def 1 ; :: thesis: verum