let A, B be Category; :: thesis: ( A ~= B implies A is_equivalent_with B )
given F being Functor of A,B such that A1: F is isomorphic ; :: according to ISOCAT_1:def 4 :: thesis: A is_equivalent_with B
take F ; :: according to ISOCAT_1:def 10 :: thesis: ex G being Functor of B,A st
( G * F ~= id A & F * G ~= id B )
take F " ; :: thesis: ( (F ") * F ~= id A & F * (F ") ~= id B )
thus ( (F ") * F ~= id A & F * (F ") ~= id B ) by A1, Th11; :: thesis: verum