let A, B be Category; 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; ( 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
; ( 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
; (F ") * F = id A
thus (F ") * F =
(f ") * f
by A2, Def2
.=
id A
by A3, A1, FUNCT_1:39
; verum