let C1, C2 be non empty AltGraph ; :: thesis: for F being Contravariant FunctorStr of 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 of 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 Def14;
then consider f being Function of the carrier of C1,the carrier of C2 such that
A1: the ObjectMap of F = ~ [:f,f:] by Def3;
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:106;
then A3: F . o1 = ([:f,f:] . o1,o1) `1 by A1, FUNCT_4:def 2
.= [(f . o1),(f . o1)] `1 by FUNCT_3:96
.= f . o1 by MCART_1:7 ;
[o2,o2] in dom [:f,f:] by A2, ZFMISC_1:106;
then A4: F . o2 = ([:f,f:] . o2,o2) `1 by A1, FUNCT_4:def 2
.= [(f . o2),(f . o2)] `1 by FUNCT_3:96
.= f . o2 by MCART_1:7 ;
[o2,o1] in dom [:f,f:] by A2, ZFMISC_1:106;
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:96 ;
:: thesis: verum