let A, B be category; :: thesis: ( A,B are_isomorphic implies A,B are_equivalent )
assume A1: A,B are_isomorphic ; :: thesis: A,B are_equivalent
consider F being Functor of A,B such that
A2: ( F is bijective & F is covariant ) by A1, FUNCTOR0:def 40;
reconsider F = F as covariant Functor of A,B by A2;
consider G being Functor of B,A such that
A3: ( G = F " & G is bijective & G is covariant ) by A2, FUNCTOR0:49;
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 A2, A3, FUNCTOR1:21, FUNCTOR1:22; :: thesis: verum