let A, B be Category; :: thesis: for F being Functor of A,B st F is one-to-one holds
Obj F is one-to-one
let F be Functor of A,B; :: thesis: ( F is one-to-one implies Obj F is one-to-one )
assume A1: F is one-to-one ; :: thesis: Obj F is one-to-one
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom (Obj F) or not x2 in dom (Obj F) or not (Obj F) . x1 = (Obj F) . x2 or x1 = x2 )
assume ( x1 in dom (Obj F) & x2 in dom (Obj F) ) ; :: thesis: ( not (Obj F) . x1 = (Obj F) . x2 or x1 = x2 )
then reconsider a1 = x1, a2 = x2 as Object of A ;
assume (Obj F) . x1 = (Obj F) . x2 ; :: thesis: x1 = x2
then F . a1 = F . a2 ;
then A2: F . (id a1) = id (F . a2) by CAT_1:71
.= F . (id a2) by CAT_1:71 ;
dom F = the carrier' of A by FUNCT_2:def 1;
then id a1 = id a2 by A1, A2;
hence x1 = x2 by CAT_1:59; :: thesis: verum