let A, B be Category; :: thesis: ( ex F being Functor of A,B st F is isomorphic implies ex F being Functor of B,A st F is isomorphic )
given F being Functor of A,B such that A1: F is isomorphic ; :: thesis: ex F being Functor of B,A st F is isomorphic
take F " ; :: thesis: F " is isomorphic
thus F " is isomorphic by A1, Th8; :: thesis: verum