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 Covariant 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:] by Def2;
A7: F . o1 = [(g . o1),(g . o1)] `1 by A6, FUNCT_3:96
.= g . o1 by MCART_1:7 ;
A8: F . o2 = [(g . o2),(g . o2)] `1 by A6, FUNCT_3:96
.= g . o2 by MCART_1:7 ;
dom f' = [:the carrier of C1,the carrier of C1:] by FUNCT_2:def 1;
then (B' * f') . [o1,o2] = B' . (f' . o1,o2) by A5, FUNCT_1:23
.= the Arrows of C2 . (F . o1),(F . o2) by A1, A2, A6, A7, A8, FUNCT_3:96
.= <^(F . o1),(F . o2)^> by ALTCAT_1:def 2 ;
hence Morph-Map F,o1,o2 is Function of <^o1,o2^>,<^(F . o1),(F . o2)^> by A3, A4, A5, PBOOLE:def 18; :: thesis: verum