let C1, C2 be 1-sorted ; :: thesis: for M being BimapStr over C1,C2 st M is Contravariant & M is onto holds
M is coreflexive
let M be BimapStr over 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 ;
then consider f being Function of the carrier of C1, the carrier of C2 such that
A2: the ObjectMap of M = ~ [:f,f:] ;
the ObjectMap of M is onto by A1;
then [:f,f:] is onto by A2, Th13;
then A3: f is onto by Th4;
the ObjectMap of M .: (id the carrier of C1) = [:f,f:] .: (id the carrier of C1) by A2, Th3;
hence id the carrier of C2 c= the ObjectMap of M .: (id the carrier of C1) by A3, Th11; :: according to FUNCTOR0:def 9 :: thesis: verum