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 Def19;
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 Def20; :: thesis: verum