let B, A be Category; :: thesis: for F being Functor of A,B st F is isomorphic holds
for b being Object of B ex a being Object of A st F . a = b
let F be Functor of A,B; :: thesis: ( F is isomorphic implies for b being Object of B ex a being Object of A st F . a = b )
assume F is isomorphic ; :: thesis: for b being Object of B ex a being Object of A st F . a = b
then A1: rng (Obj F) = the carrier of B by CAT_1:def 22;
let b be Object of B; :: thesis: ex a being Object of A st F . a = b
consider a being set such that
A2: ( a in dom (Obj F) & (Obj F) . a = b ) by A1, FUNCT_1:def 5;
reconsider a = a as Object of A by A2;
take a ; :: thesis: F . a = b
thus F . a = b by A2; :: thesis: verum