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 ;
A3: rng (Obj F) = the carrier of B by A1;
then reconsider G = (Obj F) " as Function of the carrier of B, the carrier of A by A2, Th7, FUNCT_2:25;
A4: Obj F is one-to-one by A2, Th7;
now :: thesis: for b being Object of B holds G . b = (Obj (F ")) . b
let b be Object of B; :: thesis: G . b = (Obj (F ")) . b
F . (id (G . b)) = id ((Obj F) . (G . b)) by CAT_1:68
.= id b by A3, A4, FUNCT_1:35 ;
then id (G . b) = (F ") . (id b) by A2, FUNCT_2:26
.= (F ") . (id b) by A1, Def2 ;
hence G . b = (Obj (F ")) . b by CAT_1:67; :: thesis: verum
end;
hence (Obj F) " = Obj (F ") by FUNCT_2:63; :: thesis: verum