let C be Category; :: thesis: for D, E being Categorial Category
for F being Functor of C,D
for G being Functor of C,E st F = G holds
Obj F = Obj G
let D, E be Categorial Category; :: thesis: for F being Functor of C,D
for G being Functor of C,E st F = G holds
Obj F = Obj G
let F be Functor of C,D; :: thesis: for G being Functor of C,E st F = G holds
Obj F = Obj G
let G be Functor of C,E; :: thesis: ( F = G implies Obj F = Obj G )
assume A1: F = G ; :: thesis: Obj F = Obj G

A2: now

let x be set ; :: thesis: ( x in the carrier of C implies (Obj F) . x = (Obj G) . x )
assume x in the carrier of C ; :: thesis: (Obj F) . x = (Obj G) . x
then reconsider a = x as Object of C ;
A3: a = dom (id a) by CAT_1:19;
hence (Obj F) . x = dom (F . (id a)) by CAT_1:69
.= (F . (id a)) `11 by CAT_5:13
.= dom (G . (id a)) by A1, CAT_5:13
.= (Obj G) . x by A3, CAT_1:69 ;
:: thesis: verum

end;

( dom (Obj F) = the carrier of C & dom (Obj G) = the carrier of C ) by FUNCT_2:def 1;
hence Obj F = Obj G by A2, FUNCT_1:2; :: thesis: verum