thus ( F is isomorphic implies ( F is one-to-one & rng F = the carrier' of B ) ) ; :: thesis: ( F is one-to-one & rng F = the carrier' of B implies F is isomorphic )
assume that
A1: F is one-to-one and
A2: rng F = the carrier' of B ; :: thesis: F is isomorphic
thus ( F is one-to-one & rng F = the carrier' of B ) by A1, A2; :: according to CAT_1:def 25 :: thesis: rng (Obj F) = the carrier of B
thus rng (Obj F) c= the carrier of B ; :: according to XBOOLE_0:def 10 :: thesis: the carrier of B c= rng (Obj F)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of B or x in rng (Obj F) )
assume x in the carrier of B ; :: thesis: x in rng (Obj F)
then reconsider d = x as Object of B ;
consider f being object such that
A3: f in dom F and
A4: id d = F . f by A2, FUNCT_1:def 3;
reconsider f = f as Morphism of A by A3;
reconsider c = id (dom f) as Morphism of A ;
F . c = id (dom (id d)) by A4, CAT_1:63
.= id d ;
then ( dom (Obj F) = the carrier of A & (Obj F) . (dom f) = d ) by CAT_1:67, FUNCT_2:def 1;
hence x in rng (Obj F) by FUNCT_1:def 3; :: thesis: verum