let A, B be Category; :: thesis: for F being Functor of A,B st F is isomorphic holds
(F " ) " = F
let F be Functor of A,B; :: thesis: ( F is isomorphic implies (F " ) " = F )
reconsider f = F as Function of the carrier' of A,the carrier' of B ;
reconsider g = F " as Function of the carrier' of B,the carrier' of A ;
assume A1: F is isomorphic ; :: thesis: (F " ) " = F
then A2: F is one-to-one by CAT_1:def 22;
thus (F " ) " = g " by A1, Def2, Th13
.= (f " ) " by A1, Def2
.= F by A2, FUNCT_1:65 ; :: thesis: verum