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