let C, D be Category; :: thesis: for S being Functor of C,D holds *' S is Contravariant_Functor of C opp ,D
let S be Functor of C,D; :: thesis: *' S is Contravariant_Functor of C opp ,D
thus for c being Object of (C opp) ex d being Object of D st (*' S) . (id c) = id d :: according to OPPCAT_1:def 9 :: thesis: ( ( for f being Morphism of (C opp) holds
( (*' S) . (id (dom f)) = id (cod ((*' S) . f)) & (*' S) . (id (cod f)) = id (dom ((*' S) . f)) ) ) & ( for f, g being Morphism of (C opp) st dom g = cod f holds
(*' S) . (g (*) f) = ((*' S) . f) (*) ((*' S) . g) ) )
proof
let c be Object of (C opp); :: thesis: ex d being Object of D st (*' S) . (id c) = id d
(*' S) . (id c) = id ((Obj (*' S)) . c) by Lm23;
hence ex d being Object of D st (*' S) . (id c) = id d ; :: thesis: verum
end;
thus for f being Morphism of (C opp) holds
( (*' S) . (id (dom f)) = id (cod ((*' S) . f)) & (*' S) . (id (cod f)) = id (dom ((*' S) . f)) ) :: thesis: for f, g being Morphism of (C opp) st dom g = cod f holds
(*' S) . (g (*) f) = ((*' S) . f) (*) ((*' S) . g)
proof
let f be Morphism of (C opp); :: thesis: ( (*' S) . (id (dom f)) = id (cod ((*' S) . f)) & (*' S) . (id (cod f)) = id (dom ((*' S) . f)) )
thus (*' S) . (id (dom f)) = id ((Obj (*' S)) . (dom f)) by Lm23
.= id (cod ((*' S) . f)) by Lm24 ; :: thesis: (*' S) . (id (cod f)) = id (dom ((*' S) . f))
thus (*' S) . (id (cod f)) = id ((Obj (*' S)) . (cod f)) by Lm23
.= id (dom ((*' S) . f)) by Lm24 ; :: thesis: verum
end;
let f, g be Morphism of (C opp); :: thesis: ( dom g = cod f implies (*' S) . (g (*) f) = ((*' S) . f) (*) ((*' S) . g) )
assume A1: dom g = cod f ; :: thesis: (*' S) . (g (*) f) = ((*' S) . f) (*) ((*' S) . g)
A2: ( dom (opp f) = cod f & cod (opp g) = dom g ) ;
thus (*' S) . (g (*) f) = S . (opp (g (*) f)) by Def10
.= S . ((opp f) (*) (opp g)) by A1, Th16
.= (S . (opp f)) (*) (S . (opp g)) by A1, A2, CAT_1:64
.= ((*' S) . f) (*) (S . (opp g)) by Def10
.= ((*' S) . f) (*) ((*' S) . g) by Def10 ; :: thesis: verum