let A, B 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 ;
A4: rng f = the carrier' of B by A2;
thus F * (F ") = f * (f ") by A2, Def2
.= id B by A3, A4, FUNCT_1:39 ; :: thesis: (F ") * F = id A
thus (F ") * F = (f ") * f by A2, Def2
.= id A by A3, A1, FUNCT_1:39 ; :: thesis: verum