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