let C, D be Category; :: thesis: for S being Contravariant_Functor of C,D
for c being Object of C holds S . (id c) = id ((Obj S) . c)
let S be Contravariant_Functor of C,D; :: thesis: for c being Object of C holds S . (id c) = id ((Obj S) . c)
let c be Object of C; :: thesis: S . (id c) = id ((Obj S) . c)
ex d being Object of D st S . (id c) = id d by Def9;
hence S . (id c) = id ((Obj S) . c) by Th28; :: thesis: verum