let C, D be Category; :: thesis: for T being Functor of C,D
for c being Object of C
for d being Object of D st T . (id c) = id d holds
(Obj T) . c = d
let T be Functor of C,D; :: thesis: for c being Object of C
for d being Object of D st T . (id c) = id d holds
(Obj T) . c = d
for c being Object of C ex d being Object of D st T . (id c) = id d by Th97;
hence for c being Object of C
for d being Object of D st T . (id c) = id d holds
(Obj T) . c = d by Th102; :: thesis: verum