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