let C, D be Category; :: thesis: for T being Functor of C,D
for c being Object of C ex d being Object of D st T . (id c) = id d
let T be Functor of C,D; :: thesis: for c being Object of C ex d being Object of D st T . (id c) = id d
let c be Object of C; :: thesis: ex d being Object of D st T . (id c) = id d
consider d being Element of the carrier of D such that
A1: T . (the Id of C . c) = the Id of D . d by Def18;
( id c = the Id of C . c & id d = the Id of D . d ) ;
hence ex d being Object of D st T . (id c) = id d by A1; :: thesis: verum