let A, B be Category; :: thesis: for F being Functor of A,B st F is isomorphic holds
(Obj F) " = Obj (F " )
let F be Functor of A,B; :: thesis: ( F is isomorphic implies (Obj F) " = Obj (F " ) )
assume A1: F is isomorphic ; :: thesis: (Obj F) " = Obj (F " )
then A2: F is one-to-one by Def3;
A3: rng (Obj F) = the carrier of B by A1, CAT_1:def 22;
A4: Obj F is one-to-one by A2, Th12;
reconsider G = (Obj F) " as Function of the carrier of B,the carrier of A by A2, A3, Th12, FUNCT_2:31;

now

let b be Object of B; :: thesis: G . b = (Obj (F " )) . b
F . (id (G . b)) = id ((Obj F) . (G . b)) by CAT_1:104
.= id b by A3, A4, FUNCT_1:57 ;
then id (G . b) = (F " ) . (id b) by A2, FUNCT_2:32
.= (F " ) . (id b) by A1, Def2 ;
hence G . b = (Obj (F " )) . b by CAT_1:103; :: thesis: verum

end;

hence (Obj F) " = Obj (F " ) by FUNCT_2:113; :: thesis: verum