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 ;
thus (F ") " = g " by A1, Def2, Th8
.= (f ") " by A1, Def2
.= F by A2, FUNCT_1:43 ; :: thesis: verum