let B, C be Category; for S being Contravariant_Functor of C opp ,B holds /* S is Functor of C,B
let S be Contravariant_Functor of C opp ,B; /* S is Functor of C,B
now ( ( for c being Object of C ex d being Object of B 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
B 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)A2:
(
dom (f opp) = cod f &
cod (g opp) = dom g )
;
reconsider ff =
f as
Morphism of
dom f,
cod f by CAT_1:4;
reconsider gg =
g as
Morphism of
cod f,
cod g by A1, CAT_1:4;
A3:
(
Hom (
(dom f),
(cod f))
<> {} &
Hom (
(dom g),
(cod g))
<> {} )
by CAT_1:2;
then A4:
ff opp = f opp
by Def6;
A5:
gg opp = g opp
by Def6, A3, A1;
thus (/* S) . (g (*) f) =
S . ((g (*) f) opp)
by Def8
.=
S . ((f opp) (*) (g opp))
by A4, A5, A3, A1, Th14
.=
(S . (g opp)) (*) (S . (f opp))
by A1, A2, Def9
.=
((/* S) . g) (*) (S . (f opp))
by Def8
.=
((/* S) . g) (*) ((/* S) . f)
by Def8
;
verum end;
hence
/* S is Functor of C,B
by CAT_1:61; verum