let C1, C2 be non empty AltGraph ; for F being Contravariant FunctorStr over C1,C2
for o1, o2 being Object of C1 holds the ObjectMap of F . (o1,o2) = [(F . o2),(F . o1)]
let F be Contravariant FunctorStr over C1,C2; for o1, o2 being Object of C1 holds the ObjectMap of F . (o1,o2) = [(F . o2),(F . o1)]
let o1, o2 be Object of C1; the ObjectMap of F . (o1,o2) = [(F . o2),(F . o1)]
the ObjectMap of F is Contravariant
by Def13;
then consider f being Function of the carrier of C1, the carrier of C2 such that
A1:
the ObjectMap of F = ~ [:f,f:]
;
A2:
dom [:f,f:] = [: the carrier of C1, the carrier of C1:]
by FUNCT_2:def 1;
then
[o1,o1] in dom [:f,f:]
by ZFMISC_1:87;
then A3: F . o1 =
([:f,f:] . (o1,o1)) `1
by A1, FUNCT_4:def 2
.=
[(f . o1),(f . o1)] `1
by FUNCT_3:75
.=
f . o1
;
[o2,o2] in dom [:f,f:]
by A2, ZFMISC_1:87;
then A4: F . o2 =
([:f,f:] . (o2,o2)) `1
by A1, FUNCT_4:def 2
.=
[(f . o2),(f . o2)] `1
by FUNCT_3:75
.=
f . o2
;
[o2,o1] in dom [:f,f:]
by A2, ZFMISC_1:87;
hence the ObjectMap of F . (o1,o2) =
[:f,f:] . (o2,o1)
by A1, FUNCT_4:def 2
.=
[(F . o2),(F . o1)]
by A3, A4, FUNCT_3:75
;
verum