<^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; FUNCTOR0:def 13,FUNCTOR0:def 14 C1 --> m is feasible
let o1, o2 be object of C1; FUNCTOR0:def 12 ( <^o1,o2^> <> {} implies the Arrows of C2 . (the ObjectMap of (C1 --> m) . o1,o2) <> {} )
assume
<^o1,o2^> <> {}
; 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; verum