<^o,o^> <> {} by ALTCAT_2:def 7;
then A1: the ObjectMap of (C1 --> m) = [:the carrier of C1,the carrier of C1:] --> [o,o] by Def18;
hence ( the ObjectMap of (C1 --> m) is Covariant & the ObjectMap of (C1 --> m) is Contravariant ) by Th16; :: according to FUNCTOR0:def 13,FUNCTOR0:def 14 :: thesis: C1 --> m is feasible
let o1, o2 be object of C1; :: according to FUNCTOR0:def 12 :: thesis: ( <^o1,o2^> <> {} implies the Arrows of C2 . (the ObjectMap of (C1 --> m) . o1,o2) <> {} )
assume <^o1,o2^> <> {} ; :: thesis: the Arrows of C2 . (the ObjectMap of (C1 --> m) . o1,o2) <> {}
[o1,o2] in [:the carrier of C1,the carrier of C1:] by ZFMISC_1:106;
then the Arrows of C2 . (the ObjectMap of (C1 --> m) . o1,o2) = the Arrows of C2 . o,o by A1, FUNCOP_1:13;
hence the Arrows of C2 . (the ObjectMap of (C1 --> m) . o1,o2) <> {} by ALTCAT_2:def 6; :: thesis: verum