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