consider I2' being non empty set , B' being ManySortedSet of , f' being Function of [:the carrier of C1,the carrier of C1:],I2' such that
A1: the ObjectMap of F = f' and
A2: the Arrows of C2 = B' and
A3: the MorphMap of F is ManySortedFunction of the Arrows of C1,B' * f' by Def4;
A4: the Arrows of C1 . [o1,o2] = the Arrows of C1 . o1,o2
.= <^o1,o2^> by ALTCAT_1:def 2 ;
A5: [o1,o2] in [:the carrier of C1,the carrier of C1:] by ZFMISC_1:106;
the ObjectMap of F is Contravariant by Def14;
then consider g being Function of the carrier of C1,the carrier of C2 such that
A6: the ObjectMap of F = ~ [:g,g:] by Def3;
A7: dom f' = [: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:106;
then [o1,o1] in dom [:g,g:] by FUNCT_4:43;
then A8: F . o1 = ([:g,g:] . o1,o1) `1 by A6, FUNCT_4:def 2
.= [(g . o1),(g . o1)] `1 by FUNCT_3:96
.= g . o1 by MCART_1:7 ;
[o2,o2] in dom (~ [:g,g:]) by A1, A6, A7, ZFMISC_1:106;
then [o2,o2] in dom [:g,g:] by FUNCT_4:43;
then A9: F . o2 = ([:g,g:] . o2,o2) `1 by A6, FUNCT_4:def 2
.= [(g . o2),(g . o2)] `1 by FUNCT_3:96
.= g . o2 by MCART_1:7 ;
[o1,o2] in dom (~ [:g,g:]) by A1, A6, A7, ZFMISC_1:106;
then A10: [o2,o1] in dom [:g,g:] by FUNCT_4:43;
(B' * f') . [o1,o2] = B' . (f' . o1,o2) by A5, A7, FUNCT_1:23
.= B' . ([: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:96
.= <^(F . o2),(F . o1)^> by ALTCAT_1:def 2 ;
hence Morph-Map F,o1,o2 is Function of <^o1,o2^>,<^(F . o2),(F . o1)^> by A3, A4, A5, PBOOLE:def 18; :: thesis: verum