<^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 Def17;
hence
( the ObjectMap of (C1 --> m) is Covariant & the ObjectMap of (C1 --> m) is Contravariant )
by Th15; FUNCTOR0:def 12,FUNCTOR0:def 13 C1 --> m is feasible
let o1, o2 be Object of C1; FUNCTOR0:def 11 ( <^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:87;
then
the Arrows of C2 . ( the ObjectMap of (C1 --> m) . (o1,o2)) = the Arrows of C2 . (o,o)
by A1, FUNCOP_1:7;
hence
the Arrows of C2 . ( the ObjectMap of (C1 --> m) . (o1,o2)) <> {}
by ALTCAT_2:def 6; verum