let A, B be category; :: thesis: ( A,B are_isomorphic implies A,B are_equivalent )
assume A,B are_isomorphic ; :: thesis: A,B are_equivalent
then consider F being Functor of A,B such that
A1: ( F is bijective & F is covariant ) ;
reconsider F = F as covariant Functor of A,B by A1;
consider G being Functor of B,A such that
A2: G = F " and
A3: ( G is bijective & G is covariant ) by A1, FUNCTOR0:48;
reconsider G = G as covariant Functor of B,A by A3;
take F ; :: according to YELLOW18:def 2 :: thesis: ex G being covariant Functor of B,A st
( G * F, id A are_naturally_equivalent & F * G, id B are_naturally_equivalent )
take G ; :: thesis: ( G * F, id A are_naturally_equivalent & F * G, id B are_naturally_equivalent )
thus ( G * F, id A are_naturally_equivalent & F * G, id B are_naturally_equivalent ) by A1, A2, FUNCTOR1:18, FUNCTOR1:19; :: thesis: verum