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 Covariant by Def12;
then consider g being Function of the carrier of C1, the carrier of C2 such that
A6: the ObjectMap of F = [:g,g:] ;
A7: F . o1 = [(g . o1),(g . o1)] `1 by A6, FUNCT_3:75
.= g . o1 ;
A8: F . o2 = [(g . o2),(g . o2)] `1 by A6, FUNCT_3:75
.= g . o2 ;
dom f9 = [: the carrier of C1, the carrier of C1:] by FUNCT_2:def 1;
then (B9 * f9) . [o1,o2] = B9 . (f9 . (o1,o2)) by A5, FUNCT_1:13
.= the Arrows of C2 . ((F . o1),(F . o2)) by A1, A2, A6, A7, A8, FUNCT_3:75
.= <^(F . o1),(F . o2)^> by ALTCAT_1:def 1 ;
hence Morph-Map (F,o1,o2) is Function of <^o1,o2^>,<^(F . o1),(F . o2)^> by A3, A4, A5, PBOOLE:def 15; :: thesis: verum