consider I29 being non empty set , B9 being ManySortedSet of I29, f9 being Function of [: the carrier of C1, the carrier of C1:],I29 such that
A1: the ObjectMap of F = f9 and
A2: the Arrows of C2 = B9 and
A3: the MorphMap of F is ManySortedFunction of the Arrows of C1,B9 * f9 by Def3;
A4: the Arrows of C1 . [o1,o2] = the Arrows of C1 . (o1,o2)
.= <^o1,o2^> by ALTCAT_1:def 1 ;
A5: [o1,o2] in [: the carrier of C1, the carrier of C1:] by ZFMISC_1:87;
the ObjectMap of F is Contravariant by Def13;
then consider g being Function of the carrier of C1, the carrier of C2 such that
A6: the ObjectMap of F = ~ [:g,g:] ;
A7: dom f9 = [: the carrier of C1, the carrier of C1:] by FUNCT_2:def 1;
then [o1,o1] in dom (~ [:g,g:]) by A1, A6, ZFMISC_1:87;
then [o1,o1] in dom [:g,g:] by FUNCT_4:42;
then A8: F . o1 = ([:g,g:] . (o1,o1)) `1 by A6, FUNCT_4:def 2
.= [(g . o1),(g . o1)] `1 by FUNCT_3:75
.= g . o1 ;
[o2,o2] in dom (~ [:g,g:]) by A1, A6, A7, ZFMISC_1:87;
then [o2,o2] in dom [:g,g:] by FUNCT_4:42;
then A9: F . o2 = ([:g,g:] . (o2,o2)) `1 by A6, FUNCT_4:def 2
.= [(g . o2),(g . o2)] `1 by FUNCT_3:75
.= g . o2 ;
[o1,o2] in dom (~ [:g,g:]) by A1, A6, A7, ZFMISC_1:87;
then A10: [o2,o1] in dom [:g,g:] by FUNCT_4:42;
(B9 * f9) . [o1,o2] = B9 . (f9 . (o1,o2)) by A5, A7, FUNCT_1:13
.= B9 . ([:g,g:] . (o2,o1)) by A1, A6, A10, FUNCT_4:def 2
.= the Arrows of C2 . ((F . o2),(F . o1)) by A2, A8, A9, FUNCT_3:75
.= <^(F . o2),(F . o1)^> by ALTCAT_1:def 1 ;
hence Morph-Map (F,o1,o2) is Function of <^o1,o2^>,<^(F . o2),(F . o1)^> by A3, A4, A5, PBOOLE:def 15; :: thesis: verum