let C, D be Category; for S being Contravariant_Functor of C,D holds S *' is Functor of C,D opp
let S be Contravariant_Functor of C,D; S *' is Functor of C,D opp
now ( ( for c being Object of C ex d being Object of (D opp) st (S *') . (id c) = id d ) & ( for f being Morphism of C holds
( (S *') . (id (dom f)) = id (dom ((S *') . f)) & (S *') . (id (cod f)) = id (cod ((S *') . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
(S *') . (g (*) f) = ((S *') . g) (*) ((S *') . f) ) )thus
for
c being
Object of
C ex
d being
Object of
(D opp) st
(S *') . (id c) = id d
( ( for f being Morphism of C holds
( (S *') . (id (dom f)) = id (dom ((S *') . f)) & (S *') . (id (cod f)) = id (cod ((S *') . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
(S *') . (g (*) f) = ((S *') . g) (*) ((S *') . f) ) )thus
for
f being
Morphism of
C holds
(
(S *') . (id (dom f)) = id (dom ((S *') . f)) &
(S *') . (id (cod f)) = id (cod ((S *') . f)) )
for f, g being Morphism of C st dom g = cod f holds
(S *') . (g (*) f) = ((S *') . g) (*) ((S *') . f)let f,
g be
Morphism of
C;
( dom g = cod f implies (S *') . (g (*) f) = ((S *') . g) (*) ((S *') . f) )assume A1:
dom g = cod f
;
(S *') . (g (*) f) = ((S *') . g) (*) ((S *') . f)then A2:
dom (S . f) = cod (S . g)
by Th31;
reconsider Sff =
S . f as
Morphism of
dom (S . f),
cod (S . f) by CAT_1:4;
reconsider Sgg =
S . g as
Morphism of
dom (S . g),
cod (S . g) by CAT_1:4;
A3:
(
Hom (
(dom (S . f)),
(cod (S . f)))
<> {} &
Hom (
(dom (S . g)),
(cod (S . g)))
<> {} )
by CAT_1:2;
then A4:
Sff opp = (S . f) opp
by Def6;
A5:
Sgg opp = (S . g) opp
by A3, Def6;
thus (S *') . (g (*) f) =
(S . (g (*) f)) opp
by Def11
.=
(Sff (*) Sgg) opp
by A1, Def9
.=
(Sgg opp) (*) (Sff opp)
by A3, A2, Th14
.=
((S *') . g) (*) ((S . f) opp)
by Def11, A4, A5
.=
((S *') . g) (*) ((S *') . f)
by Def11
;
verum end;
hence
S *' is Functor of C,D opp
by CAT_1:61; verum