let B, A be Category; :: thesis: for F being Functor of A,B st F is isomorphic holds
( F * (F " ) = id B & (F " ) * F = id A )
let F be Functor of A,B; :: thesis: ( F is isomorphic implies ( F * (F " ) = id B & (F " ) * F = id A ) )
reconsider f = F as Function of the carrier' of A,the carrier' of B ;
A1: dom f = the carrier' of A by FUNCT_2:def 1;
assume A2: F is isomorphic ; :: thesis: ( F * (F " ) = id B & (F " ) * F = id A )
then A3: F is one-to-one by Def3;
A4: rng f = the carrier' of B by A2, Def3;
thus F * (F " ) = f * (f " ) by A2, Def2
.= id B by A3, A4, FUNCT_1:61 ; :: thesis: (F " ) * F = id A
thus (F " ) * F = (f " ) * f by A2, Def2
.= id A by A3, A1, FUNCT_1:61 ; :: thesis: verum