let C, B be Category; :: thesis: for S being Contravariant_Functor of C opp ,B
for c being Object of C holds (/* S) . (id c) = id ((Obj S) . (c opp ))
let S be Contravariant_Functor of C opp ,B; :: thesis: for c being Object of C holds (/* S) . (id c) = id ((Obj S) . (c opp ))
let c be Object of C; :: thesis: (/* S) . (id c) = id ((Obj S) . (c opp ))
thus (/* S) . (id c) = S . ((id c) opp ) by Def6
.= S . (id (c opp ))
.= id ((Obj S) . (c opp )) by Th32 ; :: thesis: verum