let C1, C2 be 1-sorted ; :: thesis: for M being BimapStr of C1,C2 st M is Contravariant & M is onto holds
M is coreflexive
let M be BimapStr of C1,C2; :: thesis: ( M is Contravariant & M is onto implies M is coreflexive )
assume A1: ( M is Contravariant & M is onto ) ; :: thesis: M is coreflexive
then the ObjectMap of M is Contravariant by Def14;
then consider f being Function of the carrier of C1,the carrier of C2 such that
A2: the ObjectMap of M = ~ [:f,f:] by Def3;
the ObjectMap of M is onto by A1, Def8;
then [:f,f:] is onto by A2, Th14;
then A3: f is onto by Th5;
the ObjectMap of M .: (id the carrier of C1) = [:f,f:] .: (id the carrier of C1) by A2, Th4;
hence id the carrier of C2 c= the ObjectMap of M .: (id the carrier of C1) by A3, Th12; :: according to FUNCTOR0:def 10 :: thesis: verum