let A, B 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 A1: F is isomorphic ; :: thesis: for b being Object of B ex a being Object of A st F . a = b
let b be Object of B; :: thesis: ex a being Object of A st F . a = b
rng (Obj F) = the carrier of B by A1;
then consider a being object such that
A2: a in dom (Obj F) and
A3: (Obj F) . a = b by FUNCT_1:def 3;
reconsider a = a as Object of A by A2;
take a ; :: thesis: F . a = b
thus F . a = b by A3; :: thesis: verum