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 :: thesis: for x being object st x in the carrier of C holds
(Obj F) . x = (Obj G) . x
let x be object ; :: 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) ;
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;
thus Obj F = Obj G by A2; :: thesis: verum