let C1, C2 be non empty AltGraph ; :: thesis: 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; :: thesis: 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; :: thesis: 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 ;
:: thesis: verum