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 ) )
assume A1: F is isomorphic ; :: thesis: ( F * (F " ) = id B & (F " ) * F = id A )
then A2: F is one-to-one by Def3;
reconsider f = F as Function of the carrier' of A,the carrier' of B ;
A3: dom f = the carrier' of A by FUNCT_2:def 1;
A4: rng f = the carrier' of B by A1, Def3;
thus F * (F " ) = f * (f " ) by A1, Def2
.= id B by A2, A4, FUNCT_1:61 ; :: thesis: (F " ) * F = id A
thus (F " ) * F = (f " ) * f by A1, Def2
.= id A by A2, A3, FUNCT_1:61 ; :: thesis: verum