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 A1: F is isomorphic ; :: thesis: F " is isomorphic
then A2: F is one-to-one by CAT_1:def 22;
A3: F " = F " by A1, Def2;
hence F " is one-to-one by A2, FUNCT_1:62; :: according to ISOCAT_1:def 3 :: thesis: rng (F " ) = the carrier' of A
thus rng (F " ) = dom F by A2, A3, FUNCT_1:55
.= the carrier' of A by FUNCT_2:def 1 ; :: thesis: verum