let C1, C2 be 1-sorted ; :: thesis: for M being BimapStr over C1,C2 st M is Covariant & M is onto holds
M is coreflexive
let M be BimapStr over 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 ;
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 is onto by A2, Th4;
hence id the carrier of C2 c= the ObjectMap of M .: (id the carrier of C1) by A2, Th11; :: according to FUNCTOR0:def 9 :: thesis: verum