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 D such that
A1: T . ( the Id of C . c) = the Id of D . d by Def18;
id d = the Id of D . d ;
hence ex d being Object of D st T . (id c) = id d by A1; :: thesis: verum